Mankiewicz extension on open connected domains

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension

Glues local affine-isometry charts to obtain the principal open-domain extension theorem.

Statement

Let f be a surjective isometry from an open connected subset s of a real normed space onto an open subset t of another real normed space. Then there exists a unique ambient real affine isometry equivalence A agreeing with f on all of s. Target connectedness is not a separate assumption.

Assumptions

Real normed vector spaces E and F; s is open and connected; t is open; f is a surjective isometry from s to t.

Conclusion

There is a unique ambient real affine isometry equivalence whose restriction to s is f.

Proof route

At each source point, openness of s and t supplies matching small ambient balls. The local chart theorem gives an affine isometry agreeing with f on a smaller ball around that point. These local charts agree on overlaps and therefore form a locally constant chart-valued map; connectedness of s makes it constant. The resulting global chart is the unique extension.

Main citations

• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.OpenConnected.0.MathlibAnnex.IsometryEquiv.glue_local_affine_isometry - The proof or construction of Mankiewicz extension on open connected domains uses the project declaration “Gluing locally defined affine isometries on a connected open set” at the indicated step.
• MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball - The proof or construction of Mankiewicz extension on open connected domains uses the project declaration “Local affine-isometry chart on a smaller ball” at the indicated step.

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)

Read exact source with highlighted declaration