English
If g tends to the uniformity, then f · g tends to the uniformity iff f tends to the uniformity.
Русский
Если g сходится к униформности, то f·g сходится к униформности тогда и только тогда, когда f сходится к униформности.
LaTeX
$$$\\mathrm{Tendsto}(g, l, 𝓤 α) \\rightarrow \\mathrm{Tendsto}(f \\cdot g, l, 𝓤 α) \\iff \\mathrm{Tendsto}(f, l, 𝓤 α)$$$
Lean4
/-- If `g : ι → G × G` converges to the uniformity, then any `f : ι → G × G` converges to the
uniformity iff `f * g` does. This is often useful when `g` is valued in the diagonal,
in which case its convergence is automatic. -/
@[to_additive /-- If `g : ι → G × G` converges to the uniformity, then any `f : ι → G × G`
converges to the uniformity iff `f + g` does. This is often useful when `g` is valued in the
diagonal, in which case its convergence is automatic. -/
]
theorem uniformity_mul_iff_left {ι : Type*} {f g : ι → α × α} {l : Filter ι} (hg : Tendsto g l (𝓤 α)) :
Tendsto (f * g) l (𝓤 α) ↔ Tendsto f l (𝓤 α) :=
⟨fun hfg ↦ by simpa using hfg.uniformity_mul hg.uniformity_inv, fun hf ↦ hf.uniformity_mul hg⟩
