Center transport under bounded point-reflection symmetry

MathlibAnnex.IsometryEquiv.map_center_of_reflectionInvariant

Identifies the distinguished centers of two bounded reflection-invariant subsets under an isometry equivalence.

Statement

Let f:s≃ᵢt be an isometry equivalence between subsets of real normed affine spaces. Suppose c∈s and d∈t, the source set s is bounded, and s and t are invariant under point reflection about c and d respectively. Then f(c)=d as subtype points.

Assumptions

Real normed affine spaces; source and target sets contain their centers and are invariant under reflection through those centers; the source is bounded; f is an isometry equivalence.

Conclusion

f maps the source reflection center to the target reflection center.

Proof route

Conjugate the target reflection about d by f to obtain a self-isometry g of s. Every self-isometry of the bounded source reflection space fixes c. Translating that fixed-point equation back through f shows that f(c) is fixed by reflection about d, hence equals d.

Main citations

• _private.MathlibAnnex.Analysis.Normed.Affine.Reflection.0.MathlibAnnex.IsometryEquiv.fix_center_of_bounded_pointReflection_invariant - The proof or construction of Center transport under bounded point-reflection symmetry uses the project declaration “Every self-isometry fixes the center of a bounded reflection-invariant set” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.Reflection.0.MathlibAnnex.IsometryEquiv.restrictedPointReflection - The proof or construction of Center transport under bounded point-reflection symmetry uses the project declaration “Point reflection restricted to an invariant subset” at the indicated step.

Lean source signature (exact)

theorem map_center_of_reflectionInvariant
    {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⟩

Read exact source with highlighted declaration