div' — Mathlib

English

If f and g tend to a and b respectively along a filter l, then f/g tends to a/b along l.

Русский

Пусть f и g стремятся к a и b вдоль фильтра l, тогда f/g стремится к a/b вдоль l.

LaTeX

$$$\\mathrm{Tendsto}\, f\, l\\, (\\mathcal{N} a) \\;\\to\\; \\mathrm{Tendsto}\\, g\, l\\, (\\mathcal{N} b) \\;\\Rightarrow\\; \\mathrm{Tendsto}\\bigl(x \\mapsto f(x)/g(x)\\bigr)\\, l\\, (\\mathcal{N}(a/b))$$$

Lean4

@[to_additive sub]
theorem div' {f g : α → G} {l : Filter α} {a b : G} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) :
    Tendsto (fun x => f x / g x) l (𝓝 (a / b)) :=
  (continuous_div'.tendsto (a, b)).comp (hf.prodMk_nhds hg)

Похожие утверждения