MATHLIBANNEX / CANONICAL DECLARATION CARD

Midpoint preservation on a symmetric lens

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens

theorem

Identifies the centers of two lenses without prescribing images of their foci.

Statement

Let be real normed spaces, , , and . Put , and define the target lens in similarly. Suppose and . Every bijective isometry satisfies

Assumptions

The two real normed spaces, both half-distance inequalities, and the bijective isometry between the lenses are given. The radius is common to both lenses. The foci need not themselves belong to the lenses, and no equation for their images is assumed.

Conclusion

The midpoint of the source foci is sent to the midpoint of the target foci.

Proof route

Verify membership, boundedness and reflection invariance for these exact sets, and then apply center transport.

Proof steps

  1. For , one has . Hence by Midpoint membership. The same calculation places in the target lens.

  2. The source lens is contained in and is therefore bounded. For in that lens, reflection about is , and

    This verifies Reflection invariance of a lens for the source; the identical identities with primes verify the target condition.

  3. Apply Center transport to , , centers and this same . Step 1 supplies center membership and Step 2 supplies boundedness and both invariances. Its output is exactly the asserted equation.

Main citations

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'
In the source Mathematical meaning
{x y : E} {x' y' : F} {r : ℝ} The two source foci , two target foci , and common real radius ; are real normed spaces.
(hxy : 2⁻¹ * dist x y ≤ r) The bound which puts in the source lens.
(hxy' : 2⁻¹ * dist x' y' ≤ r) The corresponding target bound .
symmetricLens x y r ≃ᵢ symmetricLens x' y' r A bijective isometry of the two intersections of closed balls. This does not require or .
midpoint_mem_symmetricLens hxy The membership proof obtained from the source half-distance bound, allowing to be evaluated at .
((f ⟨midpoint ℝ x y, midpoint_mem_symmetricLens hxy⟩ : symmetricLens x' y' r) : F) The same image point , viewed in the ambient target space .
= midpoint ℝ x' y' The conclusion that this image equals .

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

Accepted content SHA-256: 63fba5b08bdea6c6cfb55dd9ff94c1a5d7278c5aad5f2e8de3d1b8b2fe026fa6

Accepted source guide SHA-256: 75eb26b32e968f00be1f4d6353af1f25b8afd977bbc34507f2360d52666583c7

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑