compl_mul — Mathlib

English

For any P in the L-projection subtype and any Q in M, the product with the complement of P satisfies: P^c ⋅ Q = Q − P ⋅ Q.

Русский

Для любого P в подмножестве L-проекций и любого Q в M произведение на дополнение P удовлетворяет: P^c ⋅ Q = Q − P ⋅ Q.

LaTeX

$$\widehat{P^c} \cdot Q = Q - \widehat{P} \cdot Q$$

Lean4

theorem compl_mul {P : { P : M // IsLprojection X P }} {Q : M} : ↑Pᶜ * Q = Q - ↑P * Q := by
  rw [coe_compl, sub_mul, one_mul]

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