Email Gateway (Dec 06 2022 at 08:16): Email Gateway (Dec 06 2022 at 08:16):From: Tobias Nipkow <nipkow@in.tum.de>
Birkhoff's Representation Theorem for Finite Distributive Lattices
Matthew Doty
This theory proves a theorem of Birkhoff that asserts that any finite
distributive lattice is isomorphic to the set of down-sets of that lattice's
join-irreducible elements. The isomorphism preserves order, meets and joins as
well as complementation in the case the lattice is a Boolean algebra. A
consequence of this representation theorem is that every finite Boolean algebra
is isomorphic to a powerset algebra.
https://www.isa-afp.org/entries/Birkhoff_Finite_Distributive_Lattices.html
Enjoy!
smime.p7s
Last updated: Apr 25 2024 at 20:15 UTC