instContinuousSMul — Mathlib

English

The action of R on C(α, M) is continuous, providing a ContinuousSMul structure when R and M are suitably endowed.

Русский

Действие R на C(α, M) непрерывно, образуя структуру ContinuousSMul при надлежащем наделении R и M.

LaTeX

$$$ [SMul R M]\,[ContinuousSMul R M] \Rightarrow ContinuousSMul R C(α,M). $$$

Lean4

@[to_additive]
instance [TopologicalSpace R] [SMul R M] [ContinuousSMul R M] : ContinuousSMul R C(α, M) :=
  ⟨(continuous_postcomp ⟨_, continuous_smul⟩).comp continuous_prodMk_const⟩

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