Affine extension from equal-radius closed balls

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_closedBall

Extends an isometry of closed balls by first recovering the centers and then passing through the convex-interior extension theorem.

Statement

Let f be a surjective isometry between the closed balls closedBall(c,r) and closedBall(d,r) of the same radius r>0 in real normed spaces. Then f has a unique ambient real affine isometry-equivalence extension agreeing with f on the whole source closed ball.

Assumptions

Real normed vector spaces; f is an isometry equivalence between closed balls with the same radius r > 0.

Conclusion

f extends uniquely to an ambient real affine isometry equivalence.

Proof route

The center-transport theorem shows that f sends c to d because both closed balls are bounded and invariant under reflection about their centers. Distance preservation then identifies membership in the two ambient interiors, which are the corresponding open balls. The convex extension theorem completes the proof.

Main citations

• MathlibAnnex.IsometryEquiv.map_center_of_reflectionInvariant - The proof or construction of Affine extension from equal-radius closed balls uses the project declaration “Center transport under bounded point-reflection symmetry” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Ball.0.MathlibAnnex.IsometryEquiv.pointReflection_mapsTo_closedBall - The proof or construction of Affine extension from equal-radius closed balls uses the project declaration “Closed balls are invariant under center reflection” at the indicated step.
• MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex - The proof or construction of Affine extension from equal-radius closed balls uses the project declaration “Convex-set extension via ambient interiors” at the indicated step.

Lean source signature (exact)

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

Read exact source with highlighted declaration