English
There exists a local homeomorphism between a real normed space and the open unit ball, given by f(x) = (1+||x||^2)^(-1/2) x with explicit inverse.
Русский
Существует локальный гомоморфизм между вещественным нормированным пространством и открытым единичным шаром, заданный f(x) = (1+||x||^2)^(-1/2) x с явным обратным отображением.
LaTeX
$$$\exists \; f: E\to B(0,1) \text{ such that } f(x)=\bigl(1+\|x\|^2\bigr)^{-1/2}x,\; f^{-1}(y)=\bigl(1-\|y\|^2\bigr)^{-1/2}y.$$$
Lean4
/-- Local homeomorphism between a real (semi)normed space and the unit ball.
See also `Homeomorph.unitBall`. -/
@[simps -isSimp]
def univUnitBall : OpenPartialHomeomorph E E
where
toFun x := (√(1 + ‖x‖ ^ 2))⁻¹ • x
invFun y := (√(1 - ‖(y : E)‖ ^ 2))⁻¹ • (y : E)
source := univ
target := ball 0 1
map_source' x
_ := by
have : 0 < 1 + ‖x‖ ^ 2 := by positivity
rw [mem_ball_zero_iff, norm_smul, Real.norm_eq_abs, abs_inv, ← _root_.div_eq_inv_mul,
div_lt_one (abs_pos.mpr <| Real.sqrt_ne_zero'.mpr this), ← abs_norm x, ← sq_lt_sq, abs_norm, Real.sq_sqrt this.le]
exact lt_one_add _
map_target' _ _ := trivial
left_inv' x
_ := by
match_scalars
simp [norm_smul]
field_simp
simp [sq_abs, Real.sq_sqrt (zero_lt_one_add_norm_sq x).le]
right_inv' y
hy := by
have : 0 < 1 - ‖y‖ ^ 2 := by nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
match_scalars
simp [norm_smul]
field_simp
simp [field, sq_abs, Real.sq_sqrt this.le]
open_source := isOpen_univ
open_target := isOpen_ball
continuousOn_toFun := by
suffices Continuous fun (x : E) => (√(1 + ‖x‖ ^ 2))⁻¹ by fun_prop
exact Continuous.inv₀ (by fun_prop) fun x => Real.sqrt_ne_zero'.mpr (by positivity)
continuousOn_invFun :=
by
have : ∀ y ∈ ball (0 : E) 1, √(1 - ‖(y : E)‖ ^ 2) ≠ 0 := fun y hy ↦
by
rw [Real.sqrt_ne_zero']
nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
exact
ContinuousOn.smul (ContinuousOn.inv₀ (continuousOn_const.sub (continuous_norm.continuousOn.pow _)).sqrt this)
continuousOn_id
