α : Type ?u.104399
β : Type ?u.104402
γ : Type ?u.104405
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
c : ℝ≥0∞
c_ne_zero : c ≠ 0
⊢ ∀ (x : ℝ≥0∞), ContinuousAt (fun x => x * c⁻¹) x
α : Type ?u.104399
β : Type ?u.104402
γ : Type ?u.104405
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
c : ℝ≥0∞
c_ne_zero : c ≠ 0
⊢ Continuous fun x => x / c
simp_rw [div_eq_mul_inv, continuous_iff_continuousAt]
α : Type ?u.104399
β : Type ?u.104402
γ : Type ?u.104405
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
c : ℝ≥0∞
c_ne_zero : c ≠ 0
x : ℝ≥0∞
⊢ ContinuousAt (fun x => x * c⁻¹) x
α : Type ?u.104399
β : Type ?u.104402
γ : Type ?u.104405
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
c : ℝ≥0∞
c_ne_zero : c ≠ 0
⊢ ∀ (x : ℝ≥0∞), ContinuousAt (fun x => x * c⁻¹) x
intro x
no goals
α : Type ?u.104399
β : Type ?u.104402
γ : Type ?u.104405
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
c : ℝ≥0∞
c_ne_zero : c ≠ 0
x : ℝ≥0∞
⊢ ContinuousAt (fun x => x * c⁻¹) x
exact ENNReal.continuousAt_mul_const (Or.intro_left _ (inv_ne_top.mpr c_ne_zero))