n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ n fun x => ↑(↑homeomorphUnitBall x)
suffices ContDiff ℝ n fun x : E => ((1 : ℝ) + ‖x‖ ^ 2).sqrt⁻¹ by exact this.smul contDiff_id
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => sqrt (1 + ‖x‖ ^ 2)
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
refine' ContDiff.inv _ fun x => Real.sqrt_ne_zero'.mpr (h x)
no goals
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => sqrt (1 + ‖x‖ ^ 2)
exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'
no goals
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
this : ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
⊢ ContDiff ℝ n fun x => ↑(↑homeomorphUnitBall x)
exact this.smul contDiff_id
no goals
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2
positivity