Theorems · Definition · order theory

OrderEmbedding.birkhoffSet

{α : Type u_1} → [inst : DistribLattice α] → [Fintype α] → [DecidablePred SupIrred] → α ↪o Set { a // SupIrred a }

Birkhoff's Representation Theorem. Any finite distributive lattice can be embedded in a powerset lattice.

Defined in

Mathlib.Order.Birkhoff

Cited by

6 results in Mathlib

Foundations

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

Assumes

DistribLatticeFintypeDecidablePred