# Documentation

Mathlib.Analysis.NormedSpace.HomeomorphBall

# (Local) homeomorphism between a normed space and a ball #

In this file we show that a real (semi)normed vector space is homeomorphic to the unit ball.

We formalize it in two ways:

• as a Homeomorph, see Homeomorph.unitBall;
• as a LocalHomeomorph with source = Set.univ and target = Metric.ball (0 : E) 1.

While the former approach is more natural, the latter approach provides us with a globally defined inverse function which makes it easier to say that this homeomorphism is in fact a diffeomorphism.

We also show that the unit ball Metric.ball (0 : E) 1 is homeomorphic to a ball of positive radius in an affine space over E, see LocalHomeomorph.unitBallBall.

## Tags #

homeomorphism, ball

theorem LocalHomeomorph.univUnitBall_source {E : Type u_1} [] :
LocalHomeomorph.univUnitBall.toLocalEquiv.source = Set.univ
theorem LocalHomeomorph.univUnitBall_symm_apply {E : Type u_1} [] (y : E) :
↑(LocalHomeomorph.symm LocalHomeomorph.univUnitBall) y = (Real.sqrt (1 - y ^ 2))⁻¹ y
theorem LocalHomeomorph.univUnitBall_apply {E : Type u_1} [] (x : E) :
LocalHomeomorph.univUnitBall x = (Real.sqrt (1 + x ^ 2))⁻¹ x
theorem LocalHomeomorph.univUnitBall_target {E : Type u_1} [] :
LocalHomeomorph.univUnitBall.toLocalEquiv.target =

Local homeomorphism between a real (semi)normed space and the unit ball. See also Homeomorph.unitBall.

Instances For
@[simp]
theorem LocalHomeomorph.univUnitBall_apply_zero {E : Type u_1} [] :
LocalHomeomorph.univUnitBall 0 = 0
@[simp]
theorem LocalHomeomorph.univUnitBall_symm_apply_zero {E : Type u_1} [] :
↑(LocalHomeomorph.symm LocalHomeomorph.univUnitBall) 0 = 0
theorem Homeomorph.unitBall_apply_coe {E : Type u_1} [] :
∀ (a : E), ↑(Homeomorph.unitBall a) = LocalHomeomorph.univUnitBall a
theorem Homeomorph.unitBall_symm_apply {E : Type u_1} [] :
∀ (a : ↑()), ↑(Homeomorph.symm Homeomorph.unitBall) a = ↑(↑(Homeomorph.symm (LocalHomeomorph.toHomeomorphSourceTarget LocalHomeomorph.univUnitBall)) a)
def Homeomorph.unitBall {E : Type u_1} [] :
E ≃ₜ ↑()

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 LocalHomeomorph.contDiffOn_unitBall_symm for smoothness properties that hold when E is an inner-product space.

Instances For
@[simp]
theorem Homeomorph.coe_unitBall_apply_zero {E : Type u_1} [] :
↑(Homeomorph.unitBall 0) = 0
@[simp]
theorem LocalHomeomorph.unitBallBall_apply {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) (hr : 0 < r) (a : E) :
↑() a = r a +ᵥ c
@[simp]
theorem LocalHomeomorph.unitBallBall_target {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) (hr : 0 < r) :
().toLocalEquiv.target =
@[simp]
theorem LocalHomeomorph.unitBallBall_symm_apply {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) (hr : 0 < r) (a : P) :
↑() a = r⁻¹ (a -ᵥ c)
@[simp]
theorem LocalHomeomorph.unitBallBall_source {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) (hr : 0 < r) :
().toLocalEquiv.source =
def LocalHomeomorph.unitBallBall {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) (hr : 0 < r) :

Affine homeomorphism (r • · +ᵥ c) between a normed space and an add torsor over this space, interpreted as a LocalHomeomorph between Metric.ball 0 1 and Metric.ball c r.

Instances For
def LocalHomeomorph.univBall {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) :

If r > 0, then LocalHomeomorph.univBall c r is a smooth local homeomorphism with source = Set.univ and target = Metric.ball c r. Otherwise, it is the translation by c. Thus in all cases, it sends 0 to c, see LocalHomeomorph.univBall_apply_zero.

Instances For
@[simp]
theorem LocalHomeomorph.univBall_source {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) :
().toLocalEquiv.source = Set.univ
theorem LocalHomeomorph.univBall_target {E : Type u_1} [] {P : Type u_2} [] (c : P) {r : } (hr : 0 < r) :
().toLocalEquiv.target =
theorem LocalHomeomorph.ball_subset_univBall_target {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) :
().toLocalEquiv.target
@[simp]
theorem LocalHomeomorph.univBall_apply_zero {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) :
↑() 0 = c
@[simp]
theorem LocalHomeomorph.univBall_symm_apply_center {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) :
↑() c = 0
theorem LocalHomeomorph.continuous_univBall {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) :
theorem LocalHomeomorph.continuousOn_univBall_symm {E : Type u_1} [] {P : Type u_2} [] (c : P) (r : ) :