[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1
[PROOFSTEP]
have : 0 < 1 + ‖x‖ ^ 2 := by positivity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ 0 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
this : 0 < 1 + ‖x‖ ^ 2
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1
[PROOFSTEP]
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]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
this : 0 < 1 + ‖x‖ ^ 2
⊢ ‖x‖ ^ 2 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
exact lt_one_add _
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ (fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) ((fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x) = x
[PROOFSTEP]
field_simp [norm_smul, smul_smul, (zero_lt_one_add_norm_sq x).ne', sq_abs, Real.sq_sqrt (zero_lt_one_add_norm_sq x).le,
  ← Real.sqrt_div (zero_lt_one_add_norm_sq x).le]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) ((fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) y) = y
[PROOFSTEP]
have : 0 < 1 - ‖y‖ ^ 2 := by nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2
[PROOFSTEP]
nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
this : 0 < 1 - ‖y‖ ^ 2
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) ((fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) y) = y
[PROOFSTEP]
field_simp [norm_smul, smul_smul, this.ne', sq_abs, Real.sq_sqrt this.le, ← Real.sqrt_div this.le]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ContinuousOn
    ↑{ toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y = y) }
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.source
[PROOFSTEP]
suffices Continuous fun (x : E) => (1 + ‖x‖ ^ 2).sqrt⁻¹ from (this.smul continuous_id).continuousOn
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Continuous fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹
[PROOFSTEP]
refine' Continuous.inv₀ _ fun x => Real.sqrt_ne_zero'.mpr (by positivity)
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Continuous fun x => Real.sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
continuity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ContinuousOn
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.invFun
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.target
[PROOFSTEP]
have : ∀ y ∈ ball (0 : E) 1, (1 - ‖(y : E)‖ ^ 2).sqrt ≠ 0 := fun y hy ↦
  by
  rw [Real.sqrt_ne_zero']
  nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ Real.sqrt (1 - ‖y‖ ^ 2) ≠ 0
[PROOFSTEP]
rw [Real.sqrt_ne_zero']
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2
[PROOFSTEP]
nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
this : ∀ (y : E), y ∈ ball 0 1 → Real.sqrt (1 - ‖y‖ ^ 2) ≠ 0
⊢ ContinuousOn
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.invFun
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.target
[PROOFSTEP]
exact
  ContinuousOn.smul (ContinuousOn.inv₀ (continuousOn_const.sub (continuous_norm.continuousOn.pow _)).sqrt this)
    continuousOn_id
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑univUnitBall 0 = 0
[PROOFSTEP]
simp [LocalHomeomorph.univUnitBall_apply]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑(LocalHomeomorph.symm univUnitBall) 0 = 0
[PROOFSTEP]
simp [LocalHomeomorph.univUnitBall_symm_apply]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ↑(Homeomorph.trans (Homeomorph.smulOfNeZero r (_ : r ≠ 0))
          (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) ''
      ball 0 1 =
    ball c r
[PROOFSTEP]
change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (↑(IsometryEquiv.vaddConst c) ∘ fun x => r • x) '' ball 0 1 = ball c r
[PROOFSTEP]
rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball (↑(IsometryEquiv.vaddConst c) 0) ‖r‖ = ball c r
[PROOFSTEP]
simp [abs_of_pos hr]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (univBall c r).toLocalEquiv.source = univ
[PROOFSTEP]
unfold univBall
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (if h : 0 < r then
          LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
            (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
        else
          Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))).toLocalEquiv.source =
    univ
[PROOFSTEP]
split_ifs
[GOAL]
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : 0 < r
⊢ (LocalHomeomorph.trans' univUnitBall (unitBallBall c r h✝)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)).toLocalEquiv.source =
    univ
[PROOFSTEP]
rfl
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : ¬0 < r
⊢ (Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))).toLocalEquiv.source = univ
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univBall c r).toLocalEquiv.target = ball c r
[PROOFSTEP]
rw [univBall, dif_pos hr]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (LocalHomeomorph.trans' univUnitBall (unitBallBall c r hr)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)).toLocalEquiv.target =
    ball c r
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ball c r ⊆ (univBall c r).toLocalEquiv.target
[PROOFSTEP]
by_cases hr : 0 < r
[GOAL]
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball c r ⊆ (univBall c r).toLocalEquiv.target
[PROOFSTEP]
rw [univBall_target c hr]
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (univBall c r).toLocalEquiv.target
[PROOFSTEP]
rw [univBall, dif_neg hr]
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))).toLocalEquiv.target
[PROOFSTEP]
exact subset_univ _
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(univBall c r) 0 = c
[PROOFSTEP]
unfold univBall
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(if h : 0 < r then
          LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
            (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
        else Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))
      0 =
    c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : 0 < r
⊢ ↑(LocalHomeomorph.trans' univUnitBall (unitBallBall c r h✝)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target))
      0 =
    c
[PROOFSTEP]
simp
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : ¬0 < r
⊢ ↑(Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) 0 = c
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(LocalHomeomorph.symm (univBall c r)) c = 0
[PROOFSTEP]
have : 0 ∈ (univBall c r).source := by simp
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ 0 ∈ (univBall c r).toLocalEquiv.source
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
this : 0 ∈ (univBall c r).toLocalEquiv.source
⊢ ↑(LocalHomeomorph.symm (univBall c r)) c = 0
[PROOFSTEP]
simpa only [univBall_apply_zero] using (univBall c r).left_inv this
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ Continuous ↑(univBall c r)
[PROOFSTEP]
simpa [continuous_iff_continuousOn_univ] using (univBall c r).continuousOn
