English
Let α be a group with a uniform structure in which multiplication is uniformly continuous. If f : β → α and g : β → α are uniformly continuous, then the pointwise product map x ↦ f(x) · g(x) is uniformly continuous.
Русский
Пусть α — группа с униформной структурой, для которой умножение равномерно непрерывно. Если f: β → α и g: β → α равномерно непрерывны, то отображение x ↦ f(x) · g(x) равно равномерно непрерывно.
LaTeX
$$$\\mathrm{Uniformly\\;continuous}(f) \\rightarrow \\mathrm{Uniformly\\;continuous}(g) \\rightarrow \\mathrm{Uniformly\\;continuous}(x \\mapsto f(x) \\cdot g(x))$$$
Lean4
@[to_additive]
theorem mul [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) :
UniformContinuous fun x => f x * g x :=
by
have : UniformContinuous fun x => f x / (g x)⁻¹ := hf.div hg.inv
simp_all
