smul_apply

Mathlib.Topology.Algebra.ContinuousAffineMap

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

English

A restatement of scalar action on maps: (t • f) x = t • f x.

Русский

Повторение действия скаляра на отображениях: (t • f) x = t • f x.

LaTeX

$$$\forall t \in S,\ f: P \toᴬ[R] W,\ x \in P,\ (t \cdot f)(x) = t \cdot f(x)$$$

Lean4

theorem smul_apply (t : S) (f : P →ᴬ[R] W) (x : P) : (t • f) x = t • f x :=
  rfl

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

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

Разделы

Аффилиация

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