dualRestrict_leftInverse

Mathlib.LinearAlgebra.Dual.Lemmas

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

← MathLib Explorer

English

W.dualRestrict is a left inverse of W.dualLift.

Русский

W.dualRestrict является левым обратным к W.dualLift.

LaTeX

$$LeftInverse( W.dualRestrict, W.dualLift )$$

Lean4

theorem dualRestrict_leftInverse (W : Subspace K V) : Function.LeftInverse W.dualRestrict W.dualLift := fun x => by
  rw [← LinearMap.comp_apply, dualRestrict_comp_dualLift, End.one_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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