dualLift_injective

Mathlib.LinearAlgebra.Dual.Lemmas

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

English

The map W.dualLift: W* → V* is injective.

Русский

Отображение W.dualLift: W* → V* инъективно.

LaTeX

$$Injective( W.dualLift )$$

Lean4

theorem dualLift_injective : Function.Injective W.dualLift :=
  W.dualRestrict_leftInverse.injective

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

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

Разделы

Аффилиация

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