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