Order theory
Content created by Egbert Rijke, Fredrik Bakke, Ian Ray, Jonathan Prieto-Cubides, Daniel Gratzer, Elisabeth Stenholm, Fernando Chu, Maša Žaucer, Victor Blanchi, fernabnor and louismntnu.
Created on 2022-01-05.
Last modified on 2024-10-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-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.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.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-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-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).
- 2023-11-27. Elisabeth Stenholm, Daniel Gratzer and Egbert Rijke. Additions during work on material set theory in HoTT (#910).
- 2023-11-24. Egbert Rijke. Abelianization (#877).