continuousConstSMul — Mathlib

English

If α and β are spaces with a continuous constant action of M, then their product α × β (with the product topology) also carries a continuous constant M-action.

Русский

Если пространства α и β имеют непрерывное константное действие M, то их произведение α × β (с произведной топологией) также имеет непрерывное константное действие M.

LaTeX

$$$ \\mathrm{ContinuousConstSMul}(M, \\alpha) \\wedge \\mathrm{ContinuousConstSMul}(M, \\beta) \\Rightarrow \\mathrm{ContinuousConstSMul}(M, \\alpha \\times \\beta) $$$

Lean4

@[to_additive]
instance continuousConstSMul [SMul M β] [ContinuousConstSMul M β] : ContinuousConstSMul M (α × β) :=
  ⟨fun _ => (continuous_fst.const_smul _).prodMk (continuous_snd.const_smul _)⟩

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