continuousSMul — Mathlib

English

If M acts on X and on Y, then M acts continuously on X × Y with the product topology.

Русский

Если M действует на X и на Y, то M действует непрерывно на X × Y с произведённой топологией.

LaTeX

$$ContinuousSMul M (X × Y)$$

Lean4

@[to_additive]
instance continuousSMul [SMul M X] [SMul M Y] [ContinuousSMul M X] [ContinuousSMul M Y] : ContinuousSMul M (X × Y) :=
  ⟨(continuous_fst.smul (continuous_fst.comp continuous_snd)).prodMk
      (continuous_fst.smul (continuous_snd.comp continuous_snd))⟩

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