English
A non-dependent version of the above: the function space ι → M, with pointwise multiplication, inherits a continuous multiplication provided M is a topological space with a multiplication that is continuous.
Русский
Неподвзодная версия выше: пространство функций ι → M, снабжённое покоординатным умножением, наследует непрерывность умножения при условии, что M — топологическое пространство с непрерывным умножением.
LaTeX
$$$\\text{ContinuousMul}(ι \\to M)$$$
Lean4
/-- A version of `Pi.continuousMul` for non-dependent functions. It is needed because sometimes
Lean 3 fails to use `Pi.continuousMul` for non-dependent functions. -/
@[to_additive /-- A version of `Pi.continuousAdd` for non-dependent functions. It is needed
because sometimes Lean fails to use `Pi.continuousAdd` for non-dependent functions. -/
]
instance continuousMul' : ContinuousMul (ι → M) :=
Pi.continuousMul
