map_apply

Mathlib.Topology.Algebra.Module.WeakDual

URI: https://scilib.ai/kg/mathlib#WeakSpace.map_apply

English

For any f, the evaluation of the weak-space map at x equals the evaluation of f at x.

Русский

Для любого f значение отображения WeakSpace f в точке x равно значению f в x.

LaTeX

$$$(\\mathrm{WeakSpace\\_map}\\ f)(x) = f(x)$$$

Lean4

theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
  rfl

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

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

Разделы

Аффилиация

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