English
If a family of spaces X_i with group actions by M admits proper constant smul on each X_i, then the product space ∏ X_i also carries a proper constant smul by M, defined coordinatewise.
Русский
Если для каждой пространстваX_i действует константное умножение группы M и это свойство верно на каждом X_i, то на произведении ∏ X_i существует правильное константное умножение, заданное по координатам.
LaTeX
$$$\\forall i,\\; f_g|_{X_i}: X_i \\to X_i\\text{ is proper }\\Rightarrow f_g^{\\prod_i X_i}: \\prod_i X_i \\to \\prod_i X_i, (x_i)_i \\mapsto (g\\cdot x_i)_i\\text{ is proper for every } g; $$$
Lean4
instance {M ι : Type*} {X : ι → Type*} [∀ i, SMul M (X i)] [∀ i, TopologicalSpace (X i)]
[∀ i, ProperConstSMul M (X i)] : ProperConstSMul M (∀ i, X i) :=
⟨fun c ↦ .pi_map fun i ↦ isProperMap_smul c (X i)⟩
