MathlibAnnex.IsometryEquiv.existsUnique_affineExtension
theorem
Glues local affine-isometry charts using their agreement on open overlaps.
Statement
Let be real normed spaces, a nonempty connected open set, and an open set. If is a bijective isometry, there is a unique surjective real affine isometry satisfying for every .
Assumptions
The source is open, connected and nonempty; the target is open; and the specified map is a distance-preserving bijection. No completeness or finite dimensionality is required. Target connectedness is not an independent hypothesis.
Conclusion
Exactly one ambient affine isometry extends the entire given map .
Proof route
Produce charts from matching small balls. Their agreement near an overlap point forces global equality, making the chart assignment locally constant and therefore constant on the connected source.
Proof steps
At , openness gives positive radii with and . Set . Apply Construction of a local affine-isometry chart with this same and the two smaller ball inclusions to obtain a surjective affine isometry agreeing with on .
The uniqueness mechanism is Agreement on a nonempty open set determines the affine map. If affine maps agree on a nonempty open set , choose and with . For , set and . Then , so . Affinity gives
since . Cancel ; at agreement is already known. Thus on the whole ambient space.
For each chosen chart , let be a radius of agreement. If and , then
is open, contains , and is a region on which both equal . Step 2 gives globally. Thus is locally constant, exactly as required in Gluing locally agreeing affine isometries.
Choose , using nonemptiness. On a connected space a locally constant map is constant: each fiber is open and its complement, a union of other open fibers, is open. Therefore for every . Put ; the local agreement at gives . If another affine isometry has this property, it agrees with on nonempty open , so Step 2 proves uniqueness.
Main citations
Lean source signature (exact)
theorem existsUnique_affineExtension
{s : Set E} {t : Set F} (f : s ≃ᵢ t)
(hs : IsOpen s) (hsc : IsConnected s) (ht : IsOpen t) :
∃! A : E ≃ᵃⁱ[ℝ] F,
∀ x : s, A (x : E) = ((f x : t) : F)| In the source | Mathematical meaning |
|---|---|
(f : s ≃ᵢ t) |
The given bijective isometry between subsets of real normed spaces . |
(hs : IsOpen s) |
The source is open in . |
(hsc : IsConnected s) |
The source is connected and nonempty; the latter permits the choice of a base point. |
(ht : IsOpen t) |
The target is open in . |
∃! A : E ≃ᵃⁱ[ℝ] F |
There exists exactly one surjective real affine isometry satisfying the following condition. |
∀ x : s, A (x : E) = ((f x : t) : F) |
The same agrees with at every source point , with both values viewed in . |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.IsometryEquiv.existsUnique_affineExtension
Accepted content SHA-256: 28eb2e6873bebf56605ff2b80e487855fb05b555e091551238e0527fc6a2af32
Accepted source guide SHA-256: f0df0dea467c5a19caabb59459da5400b07280f36e50f8d595f61e4a41e251e2
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73