hasCompl

Mathlib.Analysis.NormedSpace.MStructure

URI: https://scilib.ai/kg/mathlib#IsLprojection.Subtype.hasCompl

English

For a single L-projection P in the subtype, the underlying algebraic complement Pᶜ corresponds to 1 − P in M.

Русский

Для L-проекции P в подтипе, соответствующий комплемент Pᶜ, равен 1 − P внутри M.

LaTeX

$$$(P:\\{P\\!:\\).\\text{val}}^\\!\\!\\!\\! = 1 - P$$$

Lean4

instance hasCompl : HasCompl { f : M // IsLprojection X f } :=
  ⟨fun P => ⟨1 - P, P.prop.Lcomplement⟩⟩

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

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

Разделы

Аффилиация

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