instMulAction

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.instMulAction

English

The pointwise action of 𝕜 on α →ᵇ β defines a genuine scalar action: (a • f)(x) = a • f(x).

Русский

Пусть действует по точкам: для f ∈ α →ᵇ β и a ∈ 𝕜, (a • f)(x) = a • f(x).

LaTeX

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

Lean4

instance instMulAction : MulAction 𝕜 (α →ᵇ β) :=
  DFunLike.coe_injective.mulAction _ coe_smul

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru