|
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.
|
|