Midpoint preservation under lens containment

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset

theorem

Restricts a set isometry and its inverse to the two contained lenses.

Statement

Let be real normed spaces, , , and a bijective isometry. Choose and . Write . If then .

Assumptions

The half-distance bound and both displayed lens inclusions are assumed for the same points, radius and isometry. There is no openness or convexity requirement on .

Conclusion

The midpoint belongs to and its image is the midpoint of the two images. The target half-distance bound is a consequence of distance preservation.

Proof route

Use both inclusions to restrict the forward and inverse maps; then apply the lens midpoint theorem to that restriction.

Proof steps

If , then and
Hence lies in the target lens. Conversely, for in that lens, the target inclusion allows to be formed, and the same two distance identities put it in the source lens. This is precisely the bijective isometry in Restriction to corresponding lenses.
Distance preservation gives . The source half-distance bound and Midpoint membership also give .
Apply Midpoint preservation between lenses to the restricted isometry, source foci , target foci and radius . Both half-distance hypotheses were checked above. Since this restriction evaluates to the original , its output is .

Main citations

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)

In the source	Mathematical meaning
`(f : s ≃ᵢ t) (x y : s) (r : ℝ)`	The bijective isometry , two points already in , and a real radius . The ambient are real normed spaces.
`(hhalf : 2⁻¹ * dist (x : E) (y : E) ≤ r)`	The source half-distance condition ; the casts use the same points in .
`symmetricLens (x : E) (y : E) r ⊆ s`	Every point satisfying both source closed-ball inequalities belongs to .
`symmetricLens ((f x : t) : F) ((f y : t) : F) r ⊆ t`	The entire lens with foci and the same radius belongs to .
`hs (midpoint_mem_symmetricLens hhalf)`	The derived proof that : first use the half-distance bound to enter the lens, then its inclusion in .
`((f ⟨midpoint ℝ (x : E) (y : E), hs (midpoint_mem_symmetricLens hhalf)⟩ : t) : F)`	The well-defined point regarded in .
`midpoint ℝ ((f x : t) : F) ((f y : t) : F)`	The conclusion equates that point with .

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset

Accepted content SHA-256: a22ad0229a763a9c4fbb846f8874c408c690b05e0fe21eb51c664fd53bc9e568

Accepted source guide SHA-256: 745bce0b99b52d2d2f0a7c54c4d5323a3cbafd4ac67bd9500839ed3d4ff6da07

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73