Lcomplement_iff

Mathlib.Analysis.NormedSpace.MStructure

URI: https://scilib.ai/kg/mathlib#IsLprojection.Lcomplement_iff

English

P is an L-projection on X if and only if 1 − P is an L-projection on X.

Русский

P — L-проекция тогда и только тогда, когда 1 − P — L-проекция на X.

LaTeX

$$$\\text{IsLprojection } X P \\ \Longleftrightarrow\\ \\text{IsLprojection } X (1-P)$$$

Lean4

theorem Lcomplement_iff (P : M) : IsLprojection X P ↔ IsLprojection X (1 - P) :=
  ⟨Lcomplement, fun h => sub_sub_cancel 1 P ▸ h.Lcomplement⟩

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

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

Разделы

Аффилиация

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