English
A lattice α is modular iff for all x,y,z ∈ α, x ∧ z ∨ y ∧ z = (x ∧ z ∨ y) ∧ z.
Русский
Решетка α модульна тогда и только тогда, когда для всех x,y,z ∈ α выполняется x ∧ z ∨ y ∧ z = (x ∧ z ∨ y) ∧ z.
LaTeX
$$$\text{IsModularLattice }\alpha \iff \forall x,y,z\in\alpha,\ (x\wedge z)\vee(y\wedge z)=(x\wedge z\vee y)\wedge z.$$$
Lean4
/-- The diamond isomorphism between the intervals `Set.Iic a` and `Set.Ici b`. -/
def IicOrderIsoIci {a b : α} (h : IsCompl a b) : Set.Iic a ≃o Set.Ici b :=
(OrderIso.setCongr (Set.Iic a) (Set.Icc (a ⊓ b) a) (h.inf_eq_bot.symm ▸ Set.Icc_bot.symm)).trans <|
(infIccOrderIsoIccSup a b).trans
(OrderIso.setCongr (Set.Icc b (a ⊔ b)) (Set.Ici b) (h.sup_eq_top.symm ▸ Set.Icc_top))
