dualLift_of_mem

Mathlib.LinearAlgebra.Dual.Lemmas

URI: https://scilib.ai/kg/mathlib#Subspace.dualLift_of_mem

English

For φ ∈ W*, (dualLift W φ)(w) = φ(w) for all w ∈ W.

Русский

Для φ ∈ W*, (dualLift W φ)(w) = φ(w) для всех w ∈ W.

LaTeX

$$$(dualLift\_W\,\phi)(w) = \phi(w)\quad (w \in W)$$$

Lean4

theorem dualLift_of_mem {φ : Module.Dual K W} {w : V} (hw : w ∈ W) : W.dualLift φ w = φ ⟨w, hw⟩ :=
  dualLift_of_subtype ⟨w, hw⟩

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

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

Разделы

Аффилиация

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