English
Every finite distributive lattice admits a Birkhoff representation: there exists a β, decidable equality on β, finite β, and a lattice homomorphism f : α → Finset β that is injective.
Русский
Любая конечная распределительная решётка обладает представлением Биркхоффа: существует β с детерминированной равенством, конечность β и инъективное гомоморфизм-отображение f: α → Finset β.
LaTeX
$$$\\exists \\beta\\, (\\_ : \\text{DecidableEq } \\beta) (\\_ : \\text{Fintype } \\beta) (f : \\mathrm{LatticeHom}\\, α\\, (\\mathrm{Finset}\\, β)), Injective f$$$
Lean4
/-- **Birkhoff's Representation Theorem**. Any finite distributive lattice can be embedded in a
powerset lattice. -/
noncomputable def birkhoffSet : LatticeHom α (Set { a : α // SupIrred a })
where
toFun := OrderEmbedding.birkhoffSet
map_sup' := OrderEmbedding.birkhoffSet_sup
map_inf' := OrderEmbedding.birkhoffSet_inf
