instIsScalarTower_1 — Mathlib

English

If 𝕜 acts boundedly on β and IsScalarTower 𝕜 β β holds, then 𝕜 acts on α →ᵇ β in a compatible way, giving IsScalarTower 𝕜 (α →ᵇ β) (α →ᵇ β).

Русский

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

LaTeX

$$$\\text{If } [IsScalarTower 𝕜 β β] \\text{ then } IsScalarTower 𝕜 (α \\to^b β) (\\alpha \\to^b β)$$$

Lean4

instance [IsScalarTower 𝕜 β β] : IsScalarTower 𝕜 (α →ᵇ β) (α →ᵇ β) where
  smul_assoc _ _ _ := ext fun _ ↦ smul_mul_assoc ..

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