MATHLIBANNEX / CANONICAL DECLARATION CARD

Center transport under bounded point-reflection symmetry

MathlibAnnex.IsometryEquiv.map_center_of_mapsTo_pointReflection

theorem

Uses a doubling argument to identify the reflection centers under a bijective isometry.

Statement

Let be real normed affine spaces, with translation spaces . For , point reflection about is ; define on similarly. Let , , choose and , and let be a bijective isometry. If is bounded and , , then .

Assumptions

The metrics come from the normed translation spaces . The centers belong to their respective subsets; is bounded; and each subset is invariant under reflection about its designated center. No convexity, openness, completeness or finite-dimensionality assumption is used.

Conclusion

The given isometry sends the designated source center to the designated target center: .

Proof route

A conjugation argument doubles the displacement of a center under a self-isometry. Boundedness forces that displacement to vanish; applying the result to the transported target reflection identifies the two centers.

Proof steps

  1. Point reflection is an involutive isometry and fixes its center. Hence the two invariance assumptions restrict and to bijective isometries of and ; this is Restriction of point reflection.

  2. For a bijective self-isometry , define

    Since , distance preservation gives

    This is the doubling calculation in Bounded reflection-center lemma.

  3. The set of numbers is bounded because both points lie in bounded . Let be its supremum. Since is again a self-isometry of , Step 2 yields for every , hence and therefore . Thus every self-isometry of fixes .

  4. Apply the preceding result to . Then

    so . A point is fixed by reflection about only when it equals ; equivalently, . Hence .

Main citations

Lean source signature (exact)

theorem map_center_of_mapsTo_pointReflection
    {s : Set P} {t : Set Q} {c : P} {d : Q} (f : s ≃ᵢ t)
    (hc : c ∈ s) (hd : d ∈ t) (hs : IsBounded s)
    (hsreflect : MapsTo (pointReflection ℝ c) s s)
    (htreflect : MapsTo (pointReflection ℝ d) t t) :
    f ⟨c, hc⟩ = ⟨d, hd⟩
In the source Mathematical meaning
{s : Set P} {t : Set Q} The source subset and target subset . The Lean names are s,t and the ambient affine spaces are P,Q.
{c : P} {d : Q} The designated centers and .
(f : s ≃ᵢ t) The distance-preserving bijection , including its inverse.
(hc : c ∈ s) (hd : d ∈ t) The two membership assumptions which allow and to be used as points of the subsets.
(hs : IsBounded s) The source set is bounded.
MapsTo (pointReflection ℝ c) s s For every , the point belongs to .
MapsTo (pointReflection ℝ d) t t For every , .
f ⟨c, hc⟩ = ⟨d, hd⟩ The conclusion in . The brackets attach membership proofs to the same points; they do not choose new centers.

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_center_of_mapsTo_pointReflection

Accepted content SHA-256: b8cb8a9ea95e7e1a6d11d698a1ab9a29b4f56c92b82d9ad7089bf1729e3102d0

Accepted source guide SHA-256: e5560bf68e7619f4440f6241472aaab5edbfe96d29e59d01bfa96685546ae7fe

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑