dualRestrict_apply

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.dualRestrict_apply

English

For φ ∈ M^*, and x ∈ W, (W.dualRestrict φ)(x) = φ(x).

Русский

Для функционала φ и вектора x ∈ W выполняется (W.dualRestrict φ)(x) = φ(x).

LaTeX

$$ (W.dualRestrict \\phi) x = \\phi(x) $$

Lean4

@[simp]
theorem dualRestrict_apply (W : Submodule R M) (φ : Module.Dual R M) (x : W) : W.dualRestrict φ x = φ (x : M) :=
  rfl

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

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

Разделы

Аффилиация

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