Intersections of closed intervals of rational numbers

Content created by Louis Wasserman.

Created on 2025-10-04.
Last modified on 2025-10-08.

module elementary-number-theory.intersections-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 elementary-number-theory.poset-closed-intervals-rational-numbers

open import foundation.binary-relations
open import foundation.identity-types
open import foundation.intersections-subtypes
open import foundation.universe-levels

open import order-theory.greatest-lower-bounds-posets
open import order-theory.intersections-closed-intervals-total-orders

Idea

Two closed intervals [a, b] and [c, d] of rational numbers intersect if a ≤ d and c ≤ b.

If [a, b] and [c, d] intersect, their intersection is itself a closed interval.

Definition

intersect-prop-closed-interval-ℚ : Relation-Prop lzero closed-interval-ℚ
intersect-prop-closed-interval-ℚ =
  intersect-prop-closed-interval-Total-Order ℚ-Total-Order

intersect-closed-interval-ℚ : Relation lzero closed-interval-ℚ
intersect-closed-interval-ℚ =
  intersect-closed-interval-Total-Order ℚ-Total-Order

Properties

Intersection is reflexive

refl-intersect-closed-interval-ℚ : is-reflexive intersect-closed-interval-ℚ
refl-intersect-closed-interval-ℚ =
  refl-intersect-closed-interval-Total-Order ℚ-Total-Order

If two intervals intersect, their intersection is a closed interval

intersection-closed-interval-ℚ :
  ([a,b] [c,d] : closed-interval-ℚ) → intersect-closed-interval-ℚ [a,b] [c,d] →
  closed-interval-ℚ
intersection-closed-interval-ℚ =
  intersection-closed-interval-Total-Order ℚ-Total-Order

is-intersection-closed-interval-ℚ :
  ([a,b] [c,d] : closed-interval-ℚ) →
  (H : intersect-closed-interval-ℚ [a,b] [c,d]) →
  subtype-closed-interval-ℚ
    ( intersection-closed-interval-ℚ [a,b] [c,d] H) ＝
  intersection-subtype
    ( subtype-closed-interval-ℚ [a,b])
    ( subtype-closed-interval-ℚ [c,d])
is-intersection-closed-interval-ℚ =
  is-intersection-closed-interval-Total-Order ℚ-Total-Order

intersect-closed-interval-intersect-subtype-ℚ :
  ([a,b] [c,d] : closed-interval-ℚ) →
  intersect-subtype
    ( subtype-closed-interval-ℚ [a,b])
    ( subtype-closed-interval-ℚ [c,d]) →
  intersect-closed-interval-ℚ [a,b] [c,d]
intersect-closed-interval-intersect-subtype-ℚ =
  intersect-closed-interval-intersect-subtype-Total-Order ℚ-Total-Order

If two closed intervals intersect, their intersection is their greatest lower bound

is-greatest-binary-lower-bound-intersection-closed-interval-ℚ :
  ([a,b] [c,d] : closed-interval-ℚ) →
  (H : intersect-closed-interval-ℚ [a,b] [c,d]) →
  is-greatest-binary-lower-bound-Poset
    ( poset-closed-interval-ℚ)
    ( [a,b])
    ( [c,d])
    ( intersection-closed-interval-ℚ [a,b] [c,d] H)
is-greatest-binary-lower-bound-intersection-closed-interval-ℚ =
  is-greatest-binary-lower-bound-intersection-closed-interval-Total-Order
    ( ℚ-Total-Order)

If two closed intervals intersect, their intersection is contained in both

abstract
  leq-left-intersection-closed-interval-ℚ :
    ([a,b] [c,d] : closed-interval-ℚ) →
    (H : intersect-closed-interval-ℚ [a,b] [c,d]) →
    leq-closed-interval-ℚ (intersection-closed-interval-ℚ [a,b] [c,d] H) [a,b]
  leq-left-intersection-closed-interval-ℚ =
    leq-left-intersection-closed-interval-Total-Order ℚ-Total-Order

  leq-right-intersection-closed-interval-ℚ :
    ([a,b] [c,d] : closed-interval-ℚ) →
    (H : intersect-closed-interval-ℚ [a,b] [c,d]) →
    leq-closed-interval-ℚ (intersection-closed-interval-ℚ [a,b] [c,d] H) [c,d]
  leq-right-intersection-closed-interval-ℚ =
    leq-right-intersection-closed-interval-Total-Order ℚ-Total-Order

Recent changes