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

### License

BSD License

### Topics

- Mathematics/Order

### Session Order_Lattice_Props

- Sup_Lattice
- Order_Duality
- Order_Lattice_Props
- Representations
- Galois_Connections
- Fixpoint_Fusion
- Closure_Operators
- Order_Lattice_Props_Loc
- Order_Lattice_Props_Wenzel

### Used by

- Quantales
- Transformer Semantics

## Cite

×

Order_Lattice_Props-AFP

    @article{Order_Lattice_Props-AFP,
      author  = {Georg Struth},
      title   = {Properties of Orderings and Lattices},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Order_Lattice_Props.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 28, 2019 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Dec 19, 2018 : Isabelle2018