English
Let ma, mb: α → ENNReal, and a, b ∈ ENNReal. If ma → a and mb → b with a ≠ 0 or b ≠ 0, and an extra nondegeneracy condition a ≠ ∞ or b ≠ ∞ holds, then ma/mb → a/b.
Русский
Пусть ma, mb: α → ENNReal и a, b ∈ ENNReal. При ma → a и mb → b, если a ≠ 0 или b ≠ 0, и при этом выполняется некоторая дополнительная невыраженность a ≠ ∞ или b ≠ ∞, тогда ma/mb → a/b.
LaTeX
$$$\\text{Tendsto} ma f (\\mathcal{N} a) \\\\ \\text{and}\\ \\text{Tendsto} mb f (\\mathcal{N} b) \\\\ \\text{and} (a \\neq 0 \\lor b \\neq 0) \\\\ \\text{and} (b \\neq \\infty \\lor a \\neq \\infty)\\Rightarrow \\\\ \\text{Tendsto} (\\lambda x. ma(x)/mb(x)) f (\\mathcal{N} (a/b)).$$$
Lean4
protected theorem div {f : Filter α} {ma : α → ℝ≥0∞} {mb : α → ℝ≥0∞} {a b : ℝ≥0∞} (hma : Tendsto ma f (𝓝 a))
(ha : a ≠ 0 ∨ b ≠ 0) (hmb : Tendsto mb f (𝓝 b)) (hb : b ≠ ∞ ∨ a ≠ ∞) :
Tendsto (fun a => ma a / mb a) f (𝓝 (a / b)) := by
apply Tendsto.mul hma _ (ENNReal.tendsto_inv_iff.2 hmb) _ <;> simp [ha, hb]
