English
Birkhoff Representation for finite distributive lattices: there is an order isomorphism between a finite distributive lattice α (with a bottom element) and the lattice of lower sets of its sup-irreducible elements.
Русский
Представление Биркхоффа для конечных распределительных решёток: существует изоморфизм порядков между конечной распределительной решёткой α и решёткой нижних множеств её суп-нередуцируемых элементов.
LaTeX
$$$\\text{lowerSetSupIrred} : α \\cong_o \\mathrm{LowerSet}\\,\\{ a : α \\mid \\mathrm{SupIrred}\\, a \\}$$$
Lean4
@[simp]
theorem supIrredLowerSet_symm_apply (s : { s : LowerSet α // SupIrred s }) [Fintype s] :
supIrredLowerSet.symm s = (s.1 : Set α).toFinset.sup id := by
classical
obtain ⟨s, hs⟩ := s
obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs
cases nonempty_fintype α
have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
simp [symm_apply_eq]
