uniformity_mul — Mathlib

English

If f and g are functions tending to the uniformity of α, then the product f · g tends to the uniformity of α.

Русский

Если функции f и g сходятся к униформности α, то произведение f · g сходится к той же униформности.

LaTeX

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

Lean4

@[to_additive]
theorem uniformity_mul {ι : Type*} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (𝓤 α)) (hg : Tendsto g l (𝓤 α)) :
    Tendsto (f * g) l (𝓤 α) :=
  have : Tendsto (fun (p : (α × α) × (α × α)) ↦ p.1 * p.2) (𝓤 α ×ˢ 𝓤 α) (𝓤 α) := by
    simpa [UniformContinuous, uniformity_prod_eq_prod] using uniformContinuous_mul (α := α)
  this.comp (hf.prodMk hg)

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