Commit 2024-03-18 20:17 15e8bbd9

View on Github →

chore(Order/Birkhoff): remove unnecessary assumption (#10924) Remove the assumption that the type be a distributive lattice when partial order suffices in Birkhoff's representation theorem. Co-authored by : Sam van Gool @samvang

Estimated changes

Modified Mathlib/Order/Birkhoff.lean

modified theorem LatticeHom.birkhoffFinset_injective

modified theorem OrderEmbedding.birkhoffSet_apply

modified theorem OrderEmbedding.birkhoffSet_inf

modified theorem OrderEmbedding.birkhoffSet_sup

modified theorem OrderEmbedding.coe_birkhoffFinset

added def OrderEmbedding.infIrredUpperSet

added theorem OrderEmbedding.infIrredUpperSet_apply

added theorem OrderEmbedding.infIrredUpperSet_surjective

added def OrderEmbedding.supIrredLowerSet

added theorem OrderEmbedding.supIrredLowerSet_apply

added theorem OrderEmbedding.supIrredLowerSet_surjective

added theorem OrderIso.infIrredUpperSet_apply

added theorem OrderIso.infIrredUpperSet_symm_apply

added theorem OrderIso.supIrredLowerSet_apply

added theorem OrderIso.supIrredLowerSet_symm_apply

Modified docs/references.bib