α : Type u_1
β : Type ?u.125858
γ : Type ?u.125861
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ⊤ ∨ a ≠ ⊤
⊢ b⁻¹ ≠ 0 ∨ a ≠ ⊤
α : Type u_1
β : Type ?u.125858
γ : Type ?u.125861
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ⊤ ∨ a ≠ ⊤
⊢ Tendsto (fun b => a / m b) f (𝓝 (a / b))
apply Tendsto.const_mul (ENNReal.tendsto_inv_iff.2 hm)
no goals
α : Type u_1
β : Type ?u.125858
γ : Type ?u.125861
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ⊤ ∨ a ≠ ⊤
⊢ b⁻¹ ≠ 0 ∨ a ≠ ⊤
simp [hb]