Commit 2023-10-30 17:26 04c1707b

View on Github →

feat: Birkhoff representation theorem (#7417) Any finite distributive lattice is isomorphic to the lattice of lower sets of its irreducible elements (and to the lattice of irreducible elements of its lower sets). In particular, it can be represented as a sublattice of some powerset algebra.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Birkhoff.lean

added theorem LatticeHom.birkhoffFinset_injective

added theorem LowerSet.supIrred_Iic

added theorem LowerSet.supIrred_iff_of_finite

added theorem OrderEmbedding.birkhoffFinset_inf

added theorem OrderEmbedding.birkhoffFinset_sup

added theorem OrderEmbedding.birkhoffSet_apply

added theorem OrderEmbedding.birkhoffSet_inf

added theorem OrderEmbedding.birkhoffSet_sup

added theorem OrderEmbedding.coe_birkhoffFinset

added theorem UpperSet.infIrred_Ici

added theorem UpperSet.infIrred_iff_of_finite

added theorem exists_birkhoff_representation.{u}

Modified Mathlib/Order/Hom/Basic.lean

added theorem OrderEmbedding.coe_ofIsEmpty

added def OrderEmbedding.ofIsEmpty