instContinuousConstSMul — Mathlib

English

If S acts on R and M with continuous constant-scalar action, then the induced action on tsze R M is continuous.

Русский

Если S действует на R и M константно скаля́рно непрерывно, то соответствующее действие на tsze R M непрерывно.

LaTeX

$$$\\operatorname{ContinuousConstSMul}(S, \\mathrm{tsze}(R,M))$$$

Lean4

instance [SMul S R] [SMul S M] [ContinuousConstSMul S R] [ContinuousConstSMul S M] : ContinuousConstSMul S (tsze R M) :=
  Prod.continuousConstSMul

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