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