English
Existence of a Birkhoff representation: for any finite α with a distributive lattice structure, there exists β and an injective lattice homomorphism from α to Finset β capturing sup-irreducibles.
Русский
Существование представления Биркхоффа: для любой конечной α с распределительной решёткой существует β и инъективный гомоморфизм α → Finset β, фиксирующий SUP Irred элементы.
LaTeX
$$$\\exists β\\,(\\_ : \\text{DecidableEq } β) (\\_ : \\text{Fintype } β) (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 birkhoffFinset : LatticeHom α (Finset { a : α // SupIrred a })
where
toFun := OrderEmbedding.birkhoffFinset
map_sup' := OrderEmbedding.birkhoffFinset_sup
map_inf' := OrderEmbedding.birkhoffFinset_inf
