(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 an OpenPartialHomeomorph 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 OpenPartialHomeomorph.unitBallBall.

Tags

homeomorphism, ball

def OpenPartialHomeomorph.univUnitBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : OpenPartialHomeomorph E E

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

theorem OpenPartialHomeomorph.univUnitBall_source {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : univUnitBall.source = Set.univ

theorem OpenPartialHomeomorph.univUnitBall_symm_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (y : E) : ↑univUnitBall.symm y = (√(1 - ‖y‖ ^ 2))⁻¹ • y

theorem OpenPartialHomeomorph.univUnitBall_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : ↑univUnitBall x = (√(1 + ‖x‖ ^ 2))⁻¹ • x

theorem OpenPartialHomeomorph.univUnitBall_target {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : univUnitBall.target = Metric.ball 0 1

@[simp]

theorem OpenPartialHomeomorph.univUnitBall_apply_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ↑univUnitBall 0 = 0

@[simp]

theorem OpenPartialHomeomorph.univUnitBall_symm_apply_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ↑univUnitBall.symm 0 = 0

def Homeomorph.unitBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : E ≃ₜ ↑(Metric.ball 0 1)

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.

theorem Homeomorph.unitBall_apply_coe {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a✝ : E) : ↑(unitBall a✝) = ↑OpenPartialHomeomorph.univUnitBall a✝

theorem Homeomorph.unitBall_symm_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a✝ : ↑(Metric.ball 0 1)) : unitBall.symm a✝ = ↑(OpenPartialHomeomorph.univUnitBall.toHomeomorphSourceTarget.symm a✝)

@[simp]

theorem Homeomorph.coe_unitBall_apply_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ↑(unitBall 0) = 0

def OpenPartialHomeomorph.unitBallBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) : OpenPartialHomeomorph E P

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

@[simp]

theorem OpenPartialHomeomorph.unitBallBall_target {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) : (unitBallBall c r hr).target = Metric.ball c r

@[simp]

theorem OpenPartialHomeomorph.unitBallBall_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) (a : E) : ↑(unitBallBall c r hr) a = r • a +ᵥ c

@[simp]

theorem OpenPartialHomeomorph.unitBallBall_source {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) : (unitBallBall c r hr).source = Metric.ball 0 1

@[simp]

theorem OpenPartialHomeomorph.unitBallBall_symm_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) (a : P) : ↑(unitBallBall c r hr).symm a = r⁻¹ • (a -ᵥ c)

def OpenPartialHomeomorph.univBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : OpenPartialHomeomorph E P

If r > 0, then OpenPartialHomeomorph.univBall c r is a smooth open partial 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 OpenPartialHomeomorph.univBall_apply_zero.

@[simp]

theorem OpenPartialHomeomorph.univBall_source {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : (univBall c r).source = Set.univ

theorem OpenPartialHomeomorph.univBall_target {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) {r : ℝ} (hr : 0 < r) : (univBall c r).target = Metric.ball c r

theorem OpenPartialHomeomorph.ball_subset_univBall_target {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : Metric.ball c r ⊆ (univBall c r).target

@[simp]

theorem OpenPartialHomeomorph.univBall_apply_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : ↑(univBall c r) 0 = c

@[simp]

theorem OpenPartialHomeomorph.univBall_symm_apply_center {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : ↑(univBall c r).symm c = 0

theorem OpenPartialHomeomorph.continuous_univBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : Continuous ↑(univBall c r)

theorem OpenPartialHomeomorph.continuousOn_univBall_symm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : ContinuousOn (↑(univBall c r).symm) (Metric.ball c r)