div — Mathlib

English

If f → a and g → b with b ≠ 0, then f/g → a/b.

Русский

Если f стремится к a, а g к b, причём b ≠ 0, тогда f/g стремится к a/b.

LaTeX

$$$\\operatorname{Tendsto} f\; l\\; (\\mathcal{N} a) \\to \\operatorname{Tendsto} g\\; l\\; (\\mathcal{N} b) \\land b \\neq 0 \\Rightarrow \\operatorname{Tendsto} (f/g)\\; l\\; (\\mathcal{N}(a/b))$$$

Lean4

theorem div {l : Filter α} {a b : G₀} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) (hy : b ≠ 0) :
    Tendsto (f / g) l (𝓝 (a / b)) := by simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ hy)

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