The poset of closed intervals of rational numbers
Content created by Louis Wasserman.
Created on 2025-10-04.
Last modified on 2025-10-06.
module elementary-number-theory.poset-closed-intervals-rational-numbers where
Imports
open import elementary-number-theory.closed-intervals-rational-numbers open import elementary-number-theory.decidable-total-order-rational-numbers open import foundation.binary-relations open import foundation.logical-equivalences open import foundation.subtypes open import foundation.universe-levels open import order-theory.closed-intervals-total-orders open import order-theory.poset-closed-intervals-total-orders open import order-theory.posets open import order-theory.preorders
Idea
The closed intervals of rational numbers form a poset under the containment relation.
Definition
leq-prop-closed-interval-ℚ : Relation-Prop lzero closed-interval-ℚ leq-prop-closed-interval-ℚ = leq-prop-closed-interval-Total-Order ℚ-Total-Order leq-closed-interval-ℚ : Relation lzero closed-interval-ℚ leq-closed-interval-ℚ = leq-closed-interval-Total-Order ℚ-Total-Order
Properties
The containment relation is a partial order
abstract refl-leq-closed-interval-ℚ : is-reflexive leq-closed-interval-ℚ refl-leq-closed-interval-ℚ = refl-leq-closed-interval-Total-Order ℚ-Total-Order transitive-leq-closed-interval-ℚ : is-transitive leq-closed-interval-ℚ transitive-leq-closed-interval-ℚ = transitive-leq-closed-interval-Total-Order ℚ-Total-Order antisymmetric-leq-closed-interval-ℚ : is-antisymmetric leq-closed-interval-ℚ antisymmetric-leq-closed-interval-ℚ = antisymmetric-leq-closed-interval-Total-Order ℚ-Total-Order poset-closed-interval-ℚ : Poset lzero lzero poset-closed-interval-ℚ = poset-closed-interval-Total-Order ℚ-Total-Order
Containment of closed intervals is equivalent to containment of subtypes
abstract leq-subtype-iff-leq-closed-interval-ℚ : ([a,b] [c,d] : closed-interval-ℚ) → ( leq-closed-interval-ℚ [a,b] [c,d] ↔ ( subtype-closed-interval-ℚ [a,b] ⊆ subtype-closed-interval-ℚ [c,d])) leq-subtype-iff-leq-closed-interval-ℚ = leq-subtype-iff-leq-closed-interval-Total-Order ℚ-Total-Order leq-subtype-leq-closed-interval-ℚ : ([a,b] [c,d] : closed-interval-ℚ) → leq-closed-interval-ℚ [a,b] [c,d] → subtype-closed-interval-ℚ [a,b] ⊆ subtype-closed-interval-ℚ [c,d] leq-subtype-leq-closed-interval-ℚ = leq-subtype-leq-closed-interval-Total-Order ℚ-Total-Order leq-closed-interval-leq-subtype-ℚ : ([a,b] [c,d] : closed-interval-ℚ) → subtype-closed-interval-ℚ [a,b] ⊆ subtype-closed-interval-ℚ [c,d] → leq-closed-interval-ℚ [a,b] [c,d] leq-closed-interval-leq-subtype-ℚ = leq-closed-interval-leq-subtype-Total-Order ℚ-Total-Order
Recent changes
- 2025-10-06. Louis Wasserman. Multiplication of closed intervals on rational numbers is subdistributive over addition (#1567).
- 2025-10-04. Louis Wasserman. Poset of closed intervals (#1563).