English
There is a distributive interaction between lattice operations and multiplication in the lattice of L-projections: a precise identity holds involving sup and inf with multiplication.
Русский
Существуют дистрибутивные соотношения между операциями решётки и умножением в множестве L-проекций: выполняется точное тождество с использованием операций на вершинах и произведения.
LaTeX
$$For P,Q,R in IsLprojection X P, ((P ∨ Q) ∧ (P ∨ R)) · (P ∨ (Q ∧ R)) = P ∨ (Q ∧ R).$$
Lean4
theorem distrib_lattice_lemma [FaithfulSMul M X] {P Q R : { P : M // IsLprojection X P }} :
((↑P : M) + ↑Pᶜ * R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ := by
rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑Pᶜ)), ← mul_assoc (R : M) (↑Q * ↑R) _, ← coe_inf Q,
(Pᶜ.prop.commute R.prop).eq, ((Q ⊓ R).prop.commute Pᶜ.prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
mul_assoc (Q : M), ← mul_assoc, mul_assoc (R : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
zero_add, add_zero, ← mul_assoc, P.prop.proj.eq, R.prop.proj.eq, ← coe_inf Q, mul_assoc,
((Q ⊓ R).prop.commute Pᶜ.prop).eq, ← mul_assoc, Pᶜ.prop.proj.eq]
/- This instance was created as an auxiliary definition when defining `Subtype.distribLattice`
all at once would cause a timeout. That is no longer the case. Keeping this as a useful shortcut.
-/
