English
If ma → a and mb → b along a filter f, with not both a and b infinite, then the sequence p ↦ ma p - mb p tends to a − b.
Русский
Если ma → a и mb → b вдоль фильтра f, причём не оба a и b равны бесконечности, то p ↦ ma p − mb p сходится к a − b.
LaTeX
$$$\\\\forall f \\; {ma mb : α \\to ENNReal} {a b : ENNReal}, \\\\ Tendsto ma f (\\\\nhds a) \\\\Rightarrow \\\\ Tendsto mb f (\\\\nhds b) \\\\Rightarrow \\\\text{Tendsto } (\\\\lambda p: ENNReal × ENNReal, ma p - mb p) f (\\\\nhds (a - b)).$$$
Lean4
protected theorem sub {f : Filter α} {ma : α → ℝ≥0∞} {mb : α → ℝ≥0∞} {a b : ℝ≥0∞} (hma : Tendsto ma f (𝓝 a))
(hmb : Tendsto mb f (𝓝 b)) (h : a ≠ ∞ ∨ b ≠ ∞) : Tendsto (fun a => ma a - mb a) f (𝓝 (a - b)) :=
show Tendsto ((fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 - p.2) ∘ fun a => (ma a, mb a)) f (𝓝 (a - b)) from
Tendsto.comp (ENNReal.tendsto_sub h) (hma.prodMk_nhds hmb)
