instIsCentralScalar — Mathlib

English

The space of bounded continuous functions from α to β carries a central scalar action of 𝕜: for every c in MulOpposite 𝕜 and every f in α →ᵇ β, the two natural scalar actions coincide pointwise.

Русский

Множество ограниченных непрерывных функций от α в β поддерживает центральное скалярное действие 𝕜: для каждого элемента в MulOpposite 𝕜 и для каждой функции f: α →ᵇ β тождественно выполняется равенство двух естественных действий на элементе функции.

LaTeX

$$$IsCentralScalar_{\\mathbb{K}}(\\alpha \\to^{\\mathrm{b}} \\beta)$$$

Lean4

instance instIsCentralScalar [SMul 𝕜ᵐᵒᵖ β] [IsCentralScalar 𝕜 β] : IsCentralScalar 𝕜 (α →ᵇ β) where
  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

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