### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Algebra

### Related publications

- Birkhoff, G. (1937). Rings of sets. Duke Mathematical Journal, 3(3). https://doi.org/10.1215/s0012-7094-37-00334-x
- B. A. Davey and H. A. Priestley, “Chapter 5. Representation: The Finite Case,” in Introduction to Lattices and Order, 2nd ed., Cambridge, UK ; New York, NY: Cambridge University Press, 2002, pp. 112–124.

### Session Birkhoff_Finite_Distributive_Lattices

- Birkhoff_Finite_Distributive_Lattices

## Cite

×

Birkhoff_Finite_Distributive_Lattices-AFP

    @article{Birkhoff_Finite_Distributive_Lattices-AFP,
      author  = {Matthew Doty},
      title   = {Birkhoff's Representation Theorem For Finite Distributive Lattices},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Birkhoff_Finite_Distributive_Lattices.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Dec 6, 2022 : Isabelle2022