Convex-set extension via ambient interiors

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

Exact Card identity

Stable Card ID: 45c4db7ff375613be920f48ef4a7427063daaa3084fa98c5dd90c595522e7428

Card revision: 1

Card SHA-256: 7dc5136edabd6e33db77b7a9f9a2122488e5b12c078056cb01de6e0ab95ce426

Exact public projection