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:

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 PartialHomeomorph.unitBallBall.

Tags #

homeomorphism, ball

theorem PartialHomeomorph.univUnitBall_source {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] :
PartialHomeomorph.univUnitBall.source = Set.univ
theorem PartialHomeomorph.univUnitBall_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] (x : E) :
PartialHomeomorph.univUnitBall x = ((1 + x ^ 2))⁻¹ x
theorem PartialHomeomorph.univUnitBall_target {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] :
PartialHomeomorph.univUnitBall.target = Metric.ball 0 1
theorem PartialHomeomorph.univUnitBall_symm_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] (y : E) :
PartialHomeomorph.univUnitBall.symm y = ((1 - y ^ 2))⁻¹ y

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem PartialHomeomorph.univUnitBall_apply_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] :
    PartialHomeomorph.univUnitBall 0 = 0
    @[simp]
    theorem PartialHomeomorph.univUnitBall_symm_apply_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] :
    PartialHomeomorph.univUnitBall.symm 0 = 0
    theorem Homeomorph.unitBall_apply_coe {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] :
    ∀ (a : E), (Homeomorph.unitBall a) = PartialHomeomorph.univUnitBall a
    theorem Homeomorph.unitBall_symm_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] :
    ∀ (a : (Metric.ball 0 1)), Homeomorph.unitBall.symm a = (PartialHomeomorph.univUnitBall.toHomeomorphSourceTarget.symm a)

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

    Equations
    • Homeomorph.unitBall = (Homeomorph.Set.univ E).symm.trans PartialHomeomorph.univUnitBall.toHomeomorphSourceTarget
    Instances For
      @[simp]
      theorem Homeomorph.coe_unitBall_apply_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] :
      (Homeomorph.unitBall 0) = 0
      @[simp]
      theorem PartialHomeomorph.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) :
      @[simp]
      @[simp]
      @[simp]
      theorem PartialHomeomorph.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) :
      (PartialHomeomorph.unitBallBall c r hr).symm a = r⁻¹ (a -ᵥ c)

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

      Equations
      Instances For

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

        Equations
        Instances For
          @[simp]
          theorem PartialHomeomorph.univBall_source {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ) :
          (PartialHomeomorph.univBall c r).source = Set.univ