α : Type u_1
β : Type ?u.126772
γ : Type ?u.126775
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 (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ a ≠ 0 ∨ b⁻¹ ≠ ⊤
α : Type u_1
β : Type ?u.126772
γ : Type ?u.126775
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 (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x => m x / b) f (𝓝 (a / b))
apply Tendsto.mul_const hm
no goals
α : Type u_1
β : Type ?u.126772
γ : Type ?u.126775
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 (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ a ≠ 0 ∨ b⁻¹ ≠ ⊤
simp [ha]