Proper closed intervals in the rational numbers

Content created by Louis Wasserman.

Created on 2025-10-07.
Last modified on 2025-10-07.

module elementary-number-theory.proper-closed-intervals-rational-numbers where
Imports 
open import elementary-number-theory.closed-intervals-rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

Idea

A closed interval of rational numbers is said to be proper if its lower bound is strictly less than its upper bound, or equivalently, it contains more than one element.

Definition

is-proper-prop-closed-interval-ℚ : closed-interval-ℚ → Prop lzero
is-proper-prop-closed-interval-ℚ ((a , b) , _) = le-ℚ-Prop a b

is-proper-closed-interval-ℚ : closed-interval-ℚ → UU lzero
is-proper-closed-interval-ℚ [a,b] =
  type-Prop (is-proper-prop-closed-interval-ℚ [a,b])

Recent changes