MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex
theorem
Extends agreement from a convex interior to all source points by continuity.
Statement
Let be real normed spaces and let be a bijective isometry between subsets. Assume is convex, its interior in is nonempty, and Then there is a unique surjective real affine isometry such that for every .
Assumptions
The stated interiors are ambient interiors, not relative interiors in affine spans. Convexity is assumed only for . Both directions of the displayed interior-membership equivalence are hypotheses for the given .
Conclusion
The unique ambient affine extension agrees on all of , including points outside its interior. No separate target convexity or completeness assumption is needed.
Proof route
Restrict the isometry to the two ambient interiors, use the open connected theorem, and extend equality from the dense interior inside the source set.
Proof steps
For the forward implication puts in . If , let ; the reverse implication puts in . Thus The isometry restricted to ambient interiors gives a bijective isometry , with the original forward and inverse values.
The source interior is convex and nonempty, hence connected, and both interiors are open. These verify every hypothesis of Open connected extension theorem for the restricted isometry. It yields a unique ambient affine isometry with on .
Convexity and nonempty interior give . Concretely, choose and with . For and , the point satisfies by convexity, and as . Thus the interior points are dense in the subspace , the density step used in Extension through a dense convex interior.
The two functions and are continuous. Their equality set is closed in , because is a metric space, and contains the dense interior subset. Hence for all . Any other extension restricts to an extension on the source interior; uniqueness from Step 2 makes it equal to .
Main citations
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)| In the source | Mathematical meaning |
|---|---|
(f : s ≃ᵢ t) |
The specified bijective isometry between and , with real normed spaces. |
(hs : Convex ℝ s) |
The source set is closed under real convex combinations. |
(hsint : (interior s).Nonempty) |
The ambient interior contains a point. |
(hfi : ∀ x : s, |
The next equivalence is required for every point of , for this same . |
(x : E) ∈ interior s ↔︎ ((f x : t) : F) ∈ interior t |
Exactly the ambient-interior equivalence displayed in the statement; both implications are used to restrict the forward and inverse maps. |
∃! A : E ≃ᵃⁱ[ℝ] F |
Existence and uniqueness of a surjective real affine isometry of the whole ambient spaces. |
∀ x : s, A (x : E) = ((f x : t) : F) |
The same extension agrees with on every point of , not only its interior. |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex
Accepted content SHA-256: 8d4893dc8dafda5a811b5fb7daebb9a1e9bf5eec8cd0e5b26ee341c678b80344
Accepted source guide SHA-256: d8926125e429ee9012acf47833a3008541fb229bfa58c4384d28ce2238886d48
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73