MATHLIBANNEX / CANONICAL DECLARATION CARD

Affine extension from open balls

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_ball

theorem

Applies the open connected theorem to two positive-radius balls.

Statement

Let be real normed spaces, , , and . For a bijective isometry there exists a unique surjective real affine isometry satisfying for all .

Assumptions

Both radii are positive. They are not assumed equal. No nonzero-dimension or completeness hypothesis is imposed on the spaces.

Conclusion

The specified isometry of open balls has exactly one ambient affine-isometry extension.

Proof route

Check openness and nonempty connectedness of the source ball, then substitute the two balls into the open connected theorem.

Proof steps

  1. The two balls are open. Since , , and this ball is convex: for in it and , . Thus it is nonempty and connected. Positivity of also makes the target ball nonempty and connected, although target connectedness is not an independent input to the next theorem.

  2. Apply Open connected extension theorem with , and the given . The openness and source connectedness just verified supply its hypotheses. Its single existence-and-uniqueness conclusion gives for every source-ball point, exactly as required.

Main citations

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)
In the source Mathematical meaning
{c : E} {d : F} {r R : ℝ} The two centers and two real radii in real normed spaces .
(f : ball c r ≃ᵢ ball d R) The distance-preserving bijection between open balls.
(hr : 0 < r) (hR : 0 < R) The two strict inequalities , ; no equality of radii is assumed.
∃! A : E ≃ᵃⁱ[ℝ] F A unique surjective real affine isometry of the ambient spaces satisfying the next clause.
∀ x : ball c r, A (x : E) = ((f x : ball d R) : F) For every with , the same has value .

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_ball

Accepted content SHA-256: 3660e1ed6a0b3fdd551b9c92e576b022eb7c3de869eb774474b08378cae9fb26

Accepted source guide SHA-256: a2976dcb4c535425be2e752fb173f0a9e30979f9be55212b68d39c6a0ef2f5e8

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑