Midpoint preservation on a symmetric lens

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens

Turns bounded reflection symmetry of equal-radius lenses into midpoint preservation.

Statement

Assume the midpoint of x,y belongs to symmetricLens(x,y,r), and likewise the midpoint of x′,y′ belongs to symmetricLens(x′,y′,r), as expressed by the two half-distance inequalities. Any isometry equivalence between these lenses maps midpoint(x,y) to midpoint(x′,y′).

Assumptions

Real normed vector spaces; an isometry equivalence between symmetric lenses of the same radius r; both half-distances between the respective foci are at most r.

Conclusion

The isometry maps the midpoint of the source foci to the midpoint of the target foci.

Proof route

A symmetric lens is bounded and invariant under point reflection about the midpoint of its foci. The center-transport theorem therefore sends the source midpoint to the target midpoint.

Main citations

• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.symmetricLens_reflectionInvariant - The proof or construction of Midpoint preservation on a symmetric lens uses the project declaration “A symmetric lens is invariant under reflection about its midpoint” at the indicated step.
• MathlibAnnex.IsometryEquiv.map_center_of_reflectionInvariant - The proof or construction of Midpoint preservation on a symmetric lens uses the project declaration “Center transport under bounded point-reflection symmetry” at the indicated step.
• MathlibAnnex.symmetricLens - The proof or construction of Midpoint preservation on a symmetric lens 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 on a symmetric lens 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
    {x y : E} {x' y' : F} {r : ℝ}
    (hxy : 2⁻¹ * dist x y ≤ r) (hxy' : 2⁻¹ * dist x' y' ≤ r)
    (f : symmetricLens x y r ≃ᵢ symmetricLens x' y' r) :
    ((f ⟨midpoint ℝ x y, midpoint_mem_symmetricLens hxy⟩ :
        symmetricLens x' y' r) : F) = midpoint ℝ x' y'

Read exact source with highlighted declaration