English
Existence of Birkhoff representation: for every finite α there exists β and an injective lattice homomorphism α → Finset β.
Русский
Существование представления Биркхоффа: для каждой конечной α существует β и инъективный гомоморфизм α → Finset β.
LaTeX
$$$\\exists \\beta\\, (\\_ : \\text{DecidableEq } \\beta) (\\_ : \\text{Fintype } \\beta) (f : \\mathrm{LatticeHom}\\, α\\, (\\mathrm{Finset}\\, \\beta)), Injective f$$$
Lean4
theorem exists_birkhoff_representation.{u} (α : Type u) [Finite α] [DistribLattice α] :
∃ (β : Type u) (_ : DecidableEq β) (_ : Fintype β) (f : LatticeHom α (Finset β)), Injective f := by
classical
cases nonempty_fintype α
exact ⟨{ a : α // SupIrred a }, _, inferInstance, _, LatticeHom.birkhoffFinset_injective⟩
