Bottom elements in preorders
Content created by Egbert Rijke.
Created on 2023-05-12.
Last modified on 2023-05-12.
module order-theory.bottom-elements-preorders where
Imports
open import foundation.dependent-pair-types open import foundation.propositions open import foundation.universe-levels open import order-theory.preorders
Idea
A bottom element in a preorder P
is an element b
such that b ≤ x
holds
for every element x : P
.
Definition
module _ {l1 l2 : Level} (X : Preorder l1 l2) where is-bottom-element-Preorder-Prop : type-Preorder X → Prop (l1 ⊔ l2) is-bottom-element-Preorder-Prop x = Π-Prop (type-Preorder X) (leq-Preorder-Prop X x) is-bottom-element-Preorder : type-Preorder X → UU (l1 ⊔ l2) is-bottom-element-Preorder x = type-Prop (is-bottom-element-Preorder-Prop x) is-prop-is-bottom-element-Preorder : (x : type-Preorder X) → is-prop (is-bottom-element-Preorder x) is-prop-is-bottom-element-Preorder x = is-prop-type-Prop (is-bottom-element-Preorder-Prop x) has-bottom-element-Preorder : UU (l1 ⊔ l2) has-bottom-element-Preorder = Σ (type-Preorder X) is-bottom-element-Preorder
Recent changes
- 2023-05-12. Egbert Rijke. Subframes and quotient locales via nuclei (#613).