Theorems · Inductive type · order theory

DistribLattice

Type u_1 → Type u_1

A distributive lattice is a lattice that satisfies any of four equivalent distributive properties (of sup over inf or inf over sup, on the left or right). The definition here chooses le_sup_inf: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z). To prove distributivity from the dual law, use DistribLattice.of_inf_sup_le. A classic example of a distributive lattice is the lattice of subsets of a set, and in fact this example is generic in the sense that every distributive lattice is realizable as a sublattice of a powerset lattice.

Defined in

Mathlib.Order.Lattice

Cited by

150 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms