Order theory

Files in the order theory folder

module order-theory where

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.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-posets public
open import order-theory.finite-preorders 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.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-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.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