Theorems · Definition · order theory

OrderIso.lowerSetSupIrred

{α : Type u_1} →
  [inst : DistribLattice α] → [Fintype α] → [DecidablePred SupIrred] → [OrderBot α] → α ≃o LowerSet { a // SupIrred a }

Birkhoff Representation for finite distributive lattices. Any nonempty finite distributive lattice is isomorphic to the lattice of lower sets of its sup-irreducible elements.

Defined in

Mathlib.Order.Birkhoff

Cited by

3 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DistribLatticeFintypeDecidablePredOrderBot