div — Mathlib

English

For a map f: ι → G, Cauchy (map f 𝓕) is equivalent to nontrivial 𝓕 and Tendsto of (f p.1)/(f p.2).

Русский

Для отображения f: ι → G, Cauchy (map f 𝓕) эквивалентно не тривиальному 𝓕 и предел Tendsto для (f p.1)/(f p.2).

LaTeX

$$$Cauchy(\\mathrm{map}\\ f\\ 𝓕) \\iff 𝓕 \\neq 0 \\land \\mathrm{Tendsto}\\big(\\lambda p. (f\\,p.1)/(f\\,p.2)\\big) (𝓕 \\times 𝓕) (\\mathcal{N}(1))$$$

Lean4

@[to_additive]
theorem div (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') :
    TendstoUniformlyOnFilter (f / f') (g / g') l l' := fun u hu =>
  ((uniformContinuous_div.comp_tendstoUniformlyOnFilter (hf.prodMk hf')) u hu).diag_of_prod_left

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