Lattice Properties

 

Title: Lattice Properties
Author: Viorel Preoteasa (viorel /dot/ preoteasa /at/ aalto /dot/ fi)
Submission date: 2011-09-22
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.
Change history: [2012-01-05]: 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.
BibTeX:
@article{LatticeProperties-AFP,
  author  = {Viorel Preoteasa},
  title   = {Lattice Properties},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2011,
  note    = {\url{http://isa-afp.org/entries/LatticeProperties.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Used by: DataRefinementIBP, MonoBoolTranAlgebra, PseudoHoops