Lattice Properties

Viorel Preoteasa 🌐

September 22, 2011

Abstract

This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are modular, and lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and complete lattices in general.

License

BSD License

History

January 5, 2012
Removed the theory about distributive complete lattices which is in the standard library now. Added a theory about well founded and transitive relations and a result about fixpoints in complete lattices and well founded relations. Moved the results about conjunctive and disjunctive functions to a new theory. Removed the syntactic classes for inf and sup which are in the standard library now.

Topics

Session LatticeProperties

Used by

Cite

× 
@article{LatticeProperties-AFP,
  author  = {Viorel Preoteasa},
  title   = {Lattice Properties},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2011},
  note    = {\url{https://isa-afp.org/entries/LatticeProperties.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: