# Properties of Orderings and Lattices

 Title: Properties of Orderings and Lattices Author: Georg Struth Submission date: 2018-12-11 Abstract: 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. BibTeX: @article{Order_Lattice_Props-AFP, author = {Georg Struth}, title = {Properties of Orderings and Lattices}, journal = {Archive of Formal Proofs}, month = dec, year = 2018, note = {\url{http://isa-afp.org/entries/Order_Lattice_Props.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Quantales, Transformer_Semantics