instSMulCommClass_2 — Mathlib

English

If 𝕜 acts on β, then the SMulCommClass lifts to the bounded function space: smul on α →ᵇ β commutes with scalars from 𝕜.

Русский

Если 𝕜 действует на β, то переносится на пространство ограниченных функций так, что умножение скаляров и функции коммутируют.

LaTeX

$$$SMulCommClass 𝕜 (α \\to^b β) (BoundedContinuousFunction α β)$$$

Lean4

instance [SMulCommClass 𝕜 β β] : SMulCommClass (α →ᵇ β) 𝕜 (α →ᵇ β) where smul_comm _ _ _ := ext fun _ ↦ mul_smul_comm ..

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