English
There is an embedding of a finite distributive lattice into the powerset lattice of its sup-irreducible elements, given by the map to the set of sup-irreducibles below each element.
Русский
Существует вложение конечной распределительной решётки в пашзовый набор её sup-irreducible элементов, задаваемое отображением в множество ниже-лежащих элементов.
LaTeX
$$$\\text{birkhoffSet} : α \\hookrightarrow \\mathcal{P}(\\{ a : α \\mid \\mathrm{SupIrred}(a) \\})$$$
Lean4
/-- **Birkhoff's Representation Theorem**. Any finite distributive lattice can be embedded in a
powerset lattice. -/
noncomputable def birkhoffFinset : α ↪o Finset { a : α // SupIrred a } := by
exact birkhoffSet.trans Fintype.finsetOrderIsoSet.symm.toOrderEmbedding
