English
There is an order-preserving equivalence between a finite distributive lattice and the lattice of lower sets of its sup-irreducible elements.
Русский
Существует упорядоченное эквивалентное преобразование между конечной распределительной решёткой и решёткой нижних множеств её sup-irreducible элементов.
LaTeX
$$$\\text{lowerSetSupIrred} : α \\cong_o \\mathrm{LowerSet}\\,\\{ a : α \\mid \\mathrm{SupIrred}\\, a \\}$$$
Lean4
/-- **Birkhoff's Representation Theorem**. Any finite distributive lattice can be embedded in a
powerset lattice. -/
noncomputable def birkhoffSet : α ↪o Set { a : α // SupIrred a } :=
by
by_cases h : IsEmpty α
· exact OrderEmbedding.ofIsEmpty
push_neg at h
have := Fintype.toOrderBot α
exact OrderIso.lowerSetSupIrred.toOrderEmbedding.trans ⟨⟨_, SetLike.coe_injective⟩, Iff.rfl⟩
