English
The lattice structure on the L-projection subtype is distributive: for any a,b,c in the subtype, a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c).
Русский
У распределяющейся решётки подтипа L-проекций выполняется дистрибутивное свойство: a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c).
LaTeX
$$$a \land (b \lor c) = (a \land b) \lor (a \land c).$$$
Lean4
instance distribLattice [FaithfulSMul M X] : DistribLattice { P : M // IsLprojection X P } where
le_sup_inf P Q
R :=
by
have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul, mul_add,
(Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M), (Pᶜ.prop.commute P.prop).eq,
mul_compl_self, zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq,
Pᶜ.prop.proj.eq, mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = (P : M) + ↑Q * ↑R * ↑Pᶜ := by
rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, ← compl_mul,
(Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc, distrib_lattice_lemma, (Q.prop.commute R.prop).eq,
distrib_lattice_lemma]
rw [le_def, e₁, coe_inf, e₂]
