join — Mathlib

English

The join (supremum) of two L-projections P and Q is given by P + Q − P Q, i.e., the supremum corresponds to that explicit combination.

Русский

Слияние двух L-проекций P и Q равно P + Q − P Q.

LaTeX

$$For L-projections $P,Q$, the join is given by $P\\lor Q = P+Q-PQ$.$$

Lean4

theorem join [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) :
    IsLprojection X (P + Q - P * Q) :=
  by
  convert (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1
  noncomm_ring

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