MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex
Transfers the open-connected extension theorem to convex sets whose ambient interiors are matched exactly by the isometry.
Statement
Let f be a surjective isometry from a convex subset s of a real normed space onto a subset t. Assume the ambient interior of s is nonempty and, for every x in s, x lies in interior(s) if and only if f(x) lies in interior(t). Then f extends uniquely to an ambient real affine isometry equivalence. No separate convexity assumption on t is required by this statement.
Assumptions
Real normed vector spaces; the source s is convex with nonempty interior; f is an isometry equivalence s to t; x is interior to s exactly when f(x) is interior to t.
Conclusion
f extends uniquely to an ambient real affine isometry equivalence. No additional convexity assumption on t is stated.
Proof route
Restrict f to an isometry between the two ambient interiors. Convexity and nonempty interior make the source interior connected, so the open-connected theorem yields an affine extension on the interiors. The interior of a convex set with nonempty interior is dense in the set; continuity therefore extends agreement to all of s. Uniqueness is inherited by restriction to the interior.
Proof steps
- Construct an isometry equivalence between interior(s) and interior(t) from the bidirectional interior-membership hypothesis.
- Apply the open-connected extension theorem to the two open interiors, using connectedness of the source interior obtained from convexity of s.
- Identify the subtype of points of s lying in interior(s) and prove it is dense in s via the convex closure-of-interior theorem.
- Use continuity of the affine extension and of f to extend their equality from the dense interior subtype to every point of s.
- For uniqueness, restrict any competing ambient affine isometry to the source interior and invoke the uniqueness clause from the open-connected theorem.
Main citations
- MathlibAnnex.IsometryEquiv.existsUnique_affineExtension
The proof or construction of Convex-set extension via ambient interiors uses the project declaration “Mankiewicz extension on open connected domains” at the indicated step.
- _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Convex.0.MathlibAnnex.IsometryEquiv.interiorRestriction
The proof or construction of Convex-set extension via ambient interiors uses the project declaration “Restriction of an isometry to ambient interiors” at the indicated step.
Lean source signature (exact)
theorem existsUnique_affineExtension_of_convex
{s : Set E} {t : Set F} (f : s ≃ᵢ t)
(hs : Convex ℝ s) (hsint : (interior s).Nonempty)
(hfi : ∀ x : s,
(x : E) ∈ interior s ↔ ((f x : t) : F) ∈ interior t) :
∃! A : E ≃ᵃⁱ[ℝ] F,
∀ x : s, A (x : E) = ((f x : t) : F)Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON
Exact Card identity
Stable Card ID: 45c4db7ff375613be920f48ef4a7427063daaa3084fa98c5dd90c595522e7428
Card revision: 2
Card SHA-256: e9a5e15ee95ad76de6435c37a4fee43c4bdda17836534bf186964da0c62a9c4f