continuousMul — Mathlib

English

The product of two topological monoids has a continuous multiplication; i.e., in M × N, the map ((a,b),(a',b')) ↦ (a a', b b') is continuous.

Русский

Произведение двух топологических моноид имеет непрерывное умножение; т.е. отображение $((a,b),(a',b')) \mapsto (a a', b b')$ непрерывно.

LaTeX

$$$\text{ContinuousMul}(M \times N)$$$

Lean4

@[to_additive]
instance continuousMul [TopologicalSpace N] [Mul N] [ContinuousMul N] : ContinuousMul (M × N) :=
  ⟨by apply Continuous.prodMk <;> fun_prop⟩

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