uniformity_div — Mathlib

English

If f and g tend to the uniformity, then their pointwise quotient f / g tends to the uniformity.

Русский

Если f и g сходятся к униформности, то их точечное отношение f / g сходится к униформности.

LaTeX

$$$\\mathrm{Tendsto}(f, l, 𝓤(α)) \\rightarrow \\mathrm{Tendsto}(g, l, 𝓤(α)) \\rightarrow \\mathrm{Tendsto}(f / g, l, 𝓤(α))$$$

Lean4

@[to_additive]
theorem uniformity_div {ι : Type*} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (𝓤 α)) (hg : Tendsto g l (𝓤 α)) :
    Tendsto (f / g) l (𝓤 α) := by
  rw [div_eq_mul_inv]
  exact hf.uniformity_mul hg.uniformity_inv

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