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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.