continuous_mul — Mathlib

English

The multiplication map on a topological monoid is continuous: (x,y) ↦ x·y is continuous.

Русский

Диапазон умножения в топологическом моноиде непрерывен: отображение (x,y) ↦ x·y непрерывно.

LaTeX

$$$\\text{continuous\\_mul} :\\; \\text{Continuous }(\\lambda p: M \\times M, p.1 \\cdot p.2)$$$

Lean4

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_mul : Continuous fun p : M × M => p.1 * p.2 :=
  ContinuousMul.continuous_mul

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