Midpoint preservation on a quarter ball

MathlibAnnex.IsometryEquiv.map_midpoint_of_mem_ball

Obtains a uniform local midpoint law from symmetric-lens center rigidity.

Statement

Let f:s≃ᵢt and let c∈s. Assume R>0, ball(c,R)⊆s, and ball(f(c),R)⊆t. If x,y∈s both lie in ball(c,R/4), then f sends their midpoint to the midpoint of f(x) and f(y).

Assumptions

Real normed vector spaces; radius-R balls about c and f(c) lie in the source and target; R > 0; x,y lie in the radius-R/4 source ball.

Conclusion

f sends the midpoint of x and y to the midpoint of f(x) and f(y).

Proof route

The two endpoints are less than R/2 apart. Their symmetric lens of radius R/2 lies in the source R-ball, and the corresponding target lens lies in the target R-ball. The subset-local lens theorem therefore applies.

Main citations

• MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset - The proof or construction of Midpoint preservation on a quarter ball uses the project declaration “Midpoint preservation under lens containment” at the indicated step.
• MathlibAnnex.symmetricLens - The proof or construction of Midpoint preservation on a quarter ball uses the project declaration “Symmetric lens” at the indicated step.

Lean source signature (exact)

theorem map_midpoint_of_mem_ball
    {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) {R : ℝ} (hR : 0 < R)
    (hsball : ball (c : E) R ⊆ s)
    (htball : ball ((f c : t) : F) R ⊆ t)
    (x y : s) (hx : (x : E) ∈ ball (c : E) (R / 4))
    (hy : (y : E) ∈ ball (c : E) (R / 4)) :
    ((f ⟨midpoint ℝ (x : E) (y : E),
          hsball (by
            rw [mem_ball]
            calc
              dist (midpoint ℝ (x : E) (y : E)) (c : E) ≤
                  (dist (x : E) (c : E) + dist (y : E) (c : E)) / 2 := by
                    simpa [dist_comm] using
                      dist_midpoint_midpoint_le (x : E) (y : E) (c : E) (c : E)
              _ < R := by rw [mem_ball] at hx hy; linarith)⟩ : t) : F) =
      midpoint ℝ ((f x : t) : F) ((f y : t) : F)

Read exact source with highlighted declaration