dualEquivDual_def

Mathlib.LinearAlgebra.Dual.Lemmas

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

English

The specific realization of the dual equivalence coincides with the range restriction map.

Русский

Специфическое отображение дуального эквивалентности совпадает с ограничением по диапазону.

LaTeX

$$dualEquivDual.toLinearMap = dualLift.rangeRestrict$$

Lean4

theorem dualEquivDual_def (W : Subspace K V) : W.dualEquivDual.toLinearMap = W.dualLift.rangeRestrict :=
  rfl

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

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

Разделы

Аффилиация

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