Properties of Orderings and Lattices

Georg Struth 🌐

December 11, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


These components add further fundamental order and lattice-theoretic concepts and properties to Isabelle's libraries. They follow by and large the introductory sections of the Compendium of Continuous Lattices, covering directed and filtered sets, down-closed and up-closed sets, ideals and filters, Galois connections, closure and co-closure operators. Some emphasis is on duality and morphisms between structures, as in the Compendium. To this end, three ad-hoc approaches to duality are compared.


BSD License


Session Order_Lattice_Props