dualLift_rightInverse

Mathlib.LinearAlgebra.Dual.Lemmas

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

English

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

Русский

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

LaTeX

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

Lean4

theorem dualLift_rightInverse (W : Subspace K V) : Function.RightInverse W.dualLift W.dualRestrict :=
  W.dualRestrict_leftInverse

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

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

Разделы

Аффилиация

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