English
If each γ_i carries a topological space structure, and there is a continuous constant action of M on each γ_i, then the function space ∀i γ_i (with the product topology) carries a continuous constant M-action.
Русский
Если для каждого i пространство γ_i имеет топологию и непрерывное константное действие M на γ_i, то пространство функций ∀i γ_i (с произведной топологией) также имеет непрерывное константное действие M.
LaTeX
$$$ \\bigl( \\forall i, \\mathrm{TopologicalSpace}(\\gamma_i) \\bigr) \\wedge \\bigl( \\forall i, \\mathrm{SMul}(M, \\gamma_i) \\bigr) \\wedge \\bigl( \\forall i, \\mathrm{ContinuousConstSMul}(M, \\gamma_i) \\bigr) \\Rightarrow \\mathrm{ContinuousConstSMul}(M, \\forall i, \\gamma_i) $$$
Lean4
@[to_additive]
instance {ι : Type*} {γ : ι → Type*} [∀ i, TopologicalSpace (γ i)] [∀ i, SMul M (γ i)]
[∀ i, ContinuousConstSMul M (γ i)] : ContinuousConstSMul M (∀ i, γ i) :=
⟨fun _ => continuous_pi fun i => (continuous_apply i).const_smul _⟩
