Midpoint preservation under lens containment

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset

Applies the symmetric-lens midpoint theorem inside arbitrary source and target subsets.

Statement

Let f:s≃ᵢt and x,y∈s. If the symmetric lens of radius r around x,y lies in s, the corresponding lens around f(x),f(y) lies in t, and half the distance between x and y is at most r, then f sends midpoint(x,y) to midpoint(f(x),f(y)).

Assumptions

Real normed vector spaces; f is an isometry equivalence s to t; radius-r symmetric lenses about x,y and f(x),f(y) lie in s and t; half the distance from x to y is at most r.

Conclusion

f preserves the midpoint of x and y. The target half-distance bound follows from the isometry.

Proof route

Restrict f and its inverse to the two contained lenses. Distance preservation transports the half-distance bound to the target foci. The lens-level midpoint theorem applied to this restricted isometry gives the result.

Main citations

• MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens - The proof or construction of Midpoint preservation under lens containment uses the project declaration “Midpoint preservation on a symmetric lens” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.restrictToSymmetricLens - The proof or construction of Midpoint preservation under lens containment uses the project declaration “Restriction of a set isometry to corresponding symmetric lenses” at the indicated step.
• MathlibAnnex.symmetricLens - The proof or construction of Midpoint preservation under lens containment uses the project declaration “Symmetric lens” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.midpoint_mem_symmetricLens - The proof or construction of Midpoint preservation under lens containment uses the project declaration “The midpoint belongs to a sufficiently large symmetric lens” at the indicated step.

Lean source signature (exact)

theorem map_midpoint_of_symmetricLens_subset
    {s : Set E} {t : Set F} (f : s ≃ᵢ t) (x y : s) (r : ℝ)
    (hhalf : 2⁻¹ * dist (x : E) (y : E) ≤ r)
    (hs : symmetricLens (x : E) (y : E) r ⊆ s)
    (ht : symmetricLens ((f x : t) : F) ((f y : t) : F) r ⊆ t) :
    ((f ⟨midpoint ℝ (x : E) (y : E),
          hs (midpoint_mem_symmetricLens hhalf)⟩ : t) : F) =
      midpoint ℝ ((f x : t) : F) ((f y : t) : F)

Read exact source with highlighted declaration