dualMap_apply

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.dualMap_apply

English

For linear maps f and g with x in the domain, the equality f.dualMap g x = g (f x) holds.

Русский

Для линейных отображений f и g и элемента x из исходного пространства справедливо f.dualMap g x = g(f x).

LaTeX

$$$$ f^*(g)(x) = g(f(x)) \\quad (x \\in M_1). $$$$

Lean4

@[simp]
theorem dualMap_apply (f : M₁ →ₗ[R] M₂) (g : Dual R M₂) (x : M₁) : f.dualMap g x = g (f x) :=
  rfl

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

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

Разделы

Аффилиация

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