Affine extension from open balls

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_ball

Derives the open-ball form of the Mankiewicz extension theorem from the open-connected-domain theorem.

Statement

Let f be a surjective isometry from the open ball ball(c,r) onto the open ball ball(d,R) in real normed spaces, where r>0 and R>0; the two radii need not be equal. Then there is a unique ambient real affine isometry equivalence A such that A(x)=f(x) for every x in the source ball.

Assumptions

Real normed vector spaces; f is an isometry equivalence between open balls with radii r > 0 and R > 0.

Conclusion

f extends uniquely to an ambient real affine isometry equivalence. The two positive radii need not be assumed equal.

Proof route

Both balls are open, and the source ball is connected because its radius is positive. These facts put the isometry directly within the scope of the open-connected extension theorem.

Main citations

• MathlibAnnex.IsometryEquiv.existsUnique_affineExtension - The proof or construction of Affine extension from open balls uses the project declaration “Mankiewicz extension on open connected domains” at the indicated step.

Lean source signature (exact)

theorem existsUnique_affineExtension_ball
    {c : E} {d : F} {r R : ℝ} (f : ball c r ≃ᵢ ball d R)
    (hr : 0 < r) (hR : 0 < R) :
    ∃! A : E ≃ᵃⁱ[ℝ] F,
      ∀ x : ball c r, A (x : E) = ((f x : ball d R) : F)

Read exact source with highlighted declaration