MATHLIBANNEX / CANONICAL DECLARATION CARD

Affine extension from equal-radius closed balls

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_closedBall

theorem

Recovers the centers, matches the interiors, and then extends across the boundary.

Statement

Let be real normed spaces, , , and . Write . Every bijective isometry extends uniquely to a surjective real affine isometry . The extension satisfies for every point of the source closed ball.

Assumptions

The source and target closed balls have the same positive radius . No completeness or finite dimensionality is assumed.

Conclusion

There is one and only one ambient affine isometry agreeing with the given on the entire closed ball, including its boundary.

Proof route

Use bounded reflection symmetry to send the centers to each other. The resulting distance-to-center identity verifies the interior equivalence required by the convex extension theorem.

Proof steps

  1. The centers belong to their balls since , and the source ball is bounded. Reflection through preserves its ball because , and similarly for ; see Center reflection preserves a closed ball. Apply Center transport by point reflection to these two balls and their centers to obtain .

  2. For every ,

    For a positive radius, the ambient interior of each closed ball is its corresponding open ball. Therefore

    The common radius is used in the middle equivalence.

  3. The source closed ball is convex and its interior contains . These facts and Step 2 verify Extension through a dense convex interior for the same . That theorem returns the unique ambient extension with agreement on the whole source set, so it includes the boundary points as well.

Main citations

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)
In the source Mathematical meaning
{c : E} {d : F} {r : ℝ} The two centers and one common real radius in real normed spaces .
(f : closedBall c r ≃ᵢ closedBall d r) The bijective isometry of the two closed balls with that same radius.
(hr : 0 < r) The strict positivity .
∃! A : E ≃ᵃⁱ[ℝ] F Existence and uniqueness of a surjective real affine isometry with the stated agreement.
∀ x : closedBall c r, The agreement is required for every satisfying , including boundary points.
A (x : E) = ((f x : closedBall d r) : F) The entire conclusion is at all those points, with the same .

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_closedBall

Accepted content SHA-256: 93ee3fb8ea6016e4cf22a8d0dd08598f35d25e7692b18900b60029c4bb08440a

Accepted source guide SHA-256: 5ff02130063b573e80b93db94627f81a20dada94b0e0125838e13f4defd5c9e7

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑