English
Let E be a real seminormed vector space. There exists a homeomorphism H from E onto the open unit ball B = ball(0,1) given by the explicit formula H(x) = (1 + ||x||^2)^{-1/2} · x. Equivalently, H(x) = x / sqrt(1 + ||x||^2).
Русский
Пусть E — вещественное полупоистановое векторное пространство. Существует гомеоморфизм H: E → B(0,1) (= открытый шар единицы), заданный явно H(x) = (1 + ||x||^2)^{-1/2} · x (то есть H(x) = x / sqrt(1 + ||x||^2)).
LaTeX
$$$\exists H: E \cong \mathrm{ball}(0,1) \text{ с } H(x) = \dfrac{x}{\sqrt{1+\|x\|^2}} \quad \text{для всех } x \in E.$$$
Lean4
/-- A (semi) normed real vector space is homeomorphic to the unit ball in the same space.
This homeomorphism sends `x : E` to `(1 + ‖x‖²)^(- ½) • x`.
In many cases the actual implementation is not important, so we don't mark the projection lemmas
`Homeomorph.unitBall_apply_coe` and `Homeomorph.unitBall_symm_apply` as `@[simp]`.
See also `Homeomorph.contDiff_unitBall` and `OpenPartialHomeomorph.contDiffOn_unitBall_symm`
for smoothness properties that hold when `E` is an inner-product space. -/
@[simps! -isSimp]
def unitBall : E ≃ₜ ball (0 : E) 1 :=
(Homeomorph.Set.univ _).symm.trans OpenPartialHomeomorph.univUnitBall.toHomeomorphSourceTarget
