mul_compl_self — Mathlib

English

A projection P and its complement satisfy P ⋅ P^c = 0, reflecting the disjointness of the two components.

Русский

Проекция P и её дополнение P^c удовлетворяют P ⋅ P^c = 0, что отражает раздвоенность компонент.

LaTeX

$$\widehat{P} \cdot \widehat{P^c} = 0$$

Lean4

theorem mul_compl_self {P : { P : M // IsLprojection X P }} : (↑P : M) * ↑Pᶜ = 0 := by
  rw [coe_compl, P.prop.proj.mul_one_sub_self]

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