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.
  author  = {Georg Struth},
  title   = {Properties of Orderings and Lattices},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2018,
  note    = {\url{},
            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.