smul_apply

Mathlib.Topology.ContinuousMap.Algebra

URI: https://scilib.ai/kg/mathlib#ContinuousMap.smul_apply

English

Scalar multiplication distributes pointwise on continuous maps: (c • f)(a) = c • f(a).

Русский

Скалярное умножение распределяется по точкам: (c•f)(a) = c•f(a).

LaTeX

$$$ (c\\cdot f)(a) = c\\cdot f(a) $$$

Lean4

@[to_additive]
theorem smul_apply [SMul R M] [ContinuousConstSMul R M] (c : R) (f : C(α, M)) (a : α) : (c • f) a = c • f a :=
  rfl

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

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

Разделы

Аффилиация

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