Order theory

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

Created on 2022-01-05.
Last modified on 2024-11-20.

Modules in the order theory namespace

module order-theory where

open import order-theory.accessible-elements-relations public
open import order-theory.bottom-elements-large-posets 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.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-suplattices public
open import order-theory.homomorphisms-suplattices public
open import order-theory.ideals-preorders public
open import order-theory.incidence-algebras public
open import order-theory.inflattices public
open import order-theory.inhabited-chains-posets public
open import order-theory.inhabited-chains-preorders public
open import order-theory.inhabited-finite-total-orders public
open import order-theory.interval-subposets public
open import order-theory.join-preserving-maps-posets public
open import order-theory.join-semilattices public
open import order-theory.knaster-tarski-fixed-point-theorem 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.opposite-large-posets public
open import order-theory.opposite-large-preorders public
open import order-theory.opposite-posets public
open import order-theory.opposite-preorders 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.ordinals 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.resizing-posets public
open import order-theory.resizing-preorders public
open import order-theory.resizing-suplattices 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.supremum-preserving-maps-posets 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-chains-posets 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
open import order-theory.zorns-lemma public

Recent changes

• 2024-11-20. Fredrik Bakke. Two fixed point theorems (#1227).
• 2024-11-14. Garrett Figueroa and Egbert Rijke. Incidence algebras (#1221).
• 2024-10-20. Fredrik Bakke and Egbert Rijke. Order theory from @spcfox’s modal logic (#1205).
• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 2024-08-05. Fernando Chu. Definition of ordinals (#1159).