English
Let {C_i} be a family of topological spaces each equipped with a binary operation that makes C_i into a monoid, and such that the multiplication maps are continuous in each coordinate. Then the product ∏_i C_i, with the product topology, is itself a topological monoid; equivalently, the pointwise multiplication map μ: (∏_i C_i) × (∏_i C_i) → ∏_i C_i, given by μ((x_i),(y_i)) = (x_i y_i), is continuous.
Русский
Пусть {C_i}—семейство топологических пространств, каждое из которых является моноидом с непрерывным умножением в каждой координате. Тогда произведение ∏_i C_i, оснащённое произведением топологий, тоже является топологическим моноидом; тождественно, отображение умножения по точечному произведению μ: (∏_i C_i) × (∏_i C_i) → ∏_i C_i, μ((x_i),(y_i)) = (x_i y_i), непрерывно.
LaTeX
$$$\\left(\\forall i,\\ TopologicalSpace(C_i)\\right) \\land \\left(\\forall i,\\ Mul(C_i)\\right) \\land \\left(\\forall i,\\ ContinuousMul(C_i)\\right) \\Rightarrow \\text{ContinuousMul}\\left(\\prod_{i} C_i\\right).$$$
Lean4
@[to_additive]
instance continuousMul {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Mul (C i)] [∀ i, ContinuousMul (C i)] :
ContinuousMul (∀ i, C i) where
continuous_mul := continuous_pi fun i => (continuous_apply i).fst'.mul (continuous_apply i).snd'
