uniformContinuous_mul — Mathlib

English

The map (p, q) ↦ p.1 · p.2 from α × α to α is uniformly continuous; equivalently, multiplication in a uniform group is uniformly continuous in both coordinates.

Русский

Отображение (p, q) ↦ p.1 · p.2: α × α → α равномерно непрерывно; равномерно непрерывно умножение в группе по обеим аргументам.

LaTeX

$$$\\mathrm{Uniformly\\;continuous}(\\lambda p: \\alpha \\times \\alpha.\\ p_1 \\cdot p_2)$$$

Lean4

@[to_additive]
theorem uniformContinuous_mul : UniformContinuous fun p : α × α => p.1 * p.2 :=
  uniformContinuous_fst.mul uniformContinuous_snd

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