Order theory

Content created by Egbert Rijke, Fredrik Bakke, Ian Ray, Jonathan Prieto-Cubides, Daniel Gratzer, Elisabeth Stenholm, Maša Žaucer, Victor Blanchi, fernabnor and louismntnu.

Created on 2022-01-05.
Last modified on 2023-11-27.

Files in the order theory folder

module order-theory where

open import order-theory.accessible-elements-relations public
open import order-theory.bottom-elements-posets public
open import order-theory.bottom-elements-preorders public
open import order-theory.chains-posets public
open import order-theory.chains-preorders public
open import order-theory.closure-operators-large-locales public
open import order-theory.closure-operators-large-posets public
open import order-theory.commuting-squares-of-galois-connections-large-posets public
open import order-theory.commuting-squares-of-order-preserving-maps-large-posets public
open import order-theory.coverings-locales public
open import order-theory.decidable-posets public
open import order-theory.decidable-preorders public
open import order-theory.decidable-subposets public
open import order-theory.decidable-subpreorders public
open import order-theory.decidable-total-orders public
open import order-theory.decidable-total-preorders public
open import order-theory.dependent-products-large-frames public
open import order-theory.dependent-products-large-locales public
open import order-theory.dependent-products-large-meet-semilattices public
open import order-theory.dependent-products-large-posets public
open import order-theory.dependent-products-large-preorders public
open import order-theory.dependent-products-large-suplattices public
open import order-theory.directed-complete-posets public
open import order-theory.directed-families public
open import order-theory.distributive-lattices public
open import order-theory.finite-coverings-locales public
open import order-theory.finite-posets public
open import order-theory.finite-preorders public
open import order-theory.finite-total-orders public
open import order-theory.finitely-graded-posets public
open import order-theory.frames public
open import order-theory.galois-connections public
open import order-theory.galois-connections-large-posets public
open import order-theory.greatest-lower-bounds-large-posets public
open import order-theory.greatest-lower-bounds-posets public
open import order-theory.homomorphisms-frames public
open import order-theory.homomorphisms-large-frames public
open import order-theory.homomorphisms-large-locales public
open import order-theory.homomorphisms-large-meet-semilattices public
open import order-theory.homomorphisms-large-suplattices public
open import order-theory.homomorphisms-meet-semilattices public
open import order-theory.homomorphisms-meet-sup-lattices public
open import order-theory.homomorphisms-sup-lattices public
open import order-theory.ideals-preorders public
open import order-theory.inhabited-finite-total-orders public
open import order-theory.interval-subposets public
open import order-theory.join-semilattices public
open import order-theory.large-frames public
open import order-theory.large-locales public
open import order-theory.large-meet-semilattices public
open import order-theory.large-meet-subsemilattices public
open import order-theory.large-posets public
open import order-theory.large-preorders public
open import order-theory.large-quotient-locales public
open import order-theory.large-subframes public
open import order-theory.large-subposets public
open import order-theory.large-subpreorders public
open import order-theory.large-subsuplattices public
open import order-theory.large-suplattices public
open import order-theory.lattices public
open import order-theory.least-upper-bounds-large-posets public
open import order-theory.least-upper-bounds-posets public
open import order-theory.locales public
open import order-theory.locally-finite-posets public
open import order-theory.lower-bounds-large-posets public
open import order-theory.lower-bounds-posets public
open import order-theory.lower-sets-large-posets public
open import order-theory.lower-types-preorders public
open import order-theory.maximal-chains-posets public
open import order-theory.maximal-chains-preorders public
open import order-theory.meet-semilattices public
open import order-theory.meet-suplattices public
open import order-theory.nuclei-large-locales public
open import order-theory.order-preserving-maps-large-posets public
open import order-theory.order-preserving-maps-large-preorders public
open import order-theory.order-preserving-maps-posets public
open import order-theory.order-preserving-maps-preorders public
open import order-theory.posets public
open import order-theory.powers-of-large-locales public
open import order-theory.precategory-of-decidable-total-orders public
open import order-theory.precategory-of-finite-posets public
open import order-theory.precategory-of-finite-total-orders public
open import order-theory.precategory-of-inhabited-finite-total-orders public
open import order-theory.precategory-of-posets public
open import order-theory.precategory-of-total-orders public
open import order-theory.preorders public
open import order-theory.principal-lower-sets-large-posets public
open import order-theory.principal-upper-sets-large-posets public
open import order-theory.reflective-galois-connections-large-posets public
open import order-theory.similarity-of-elements-large-posets public
open import order-theory.similarity-of-elements-large-preorders public
open import order-theory.similarity-of-order-preserving-maps-large-posets public
open import order-theory.similarity-of-order-preserving-maps-large-preorders public
open import order-theory.subposets public
open import order-theory.subpreorders public
open import order-theory.suplattices public
open import order-theory.top-elements-large-posets public
open import order-theory.top-elements-posets public
open import order-theory.top-elements-preorders public
open import order-theory.total-orders public
open import order-theory.total-preorders public
open import order-theory.upper-bounds-large-posets public
open import order-theory.upper-bounds-posets public
open import order-theory.upper-sets-large-posets public
open import order-theory.well-founded-orders public
open import order-theory.well-founded-relations public

Recent changes