Interior closed intervals in the rational numbers

Content created by Louis Wasserman.

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

module elementary-number-theory.interior-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.conjunction
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

Idea

Given two closed intervals of rational numbers [a, b] and [c, d], then [c, d] is said to be interior to [a, b] if a < c and d < b.

Definition

is-interior-prop-closed-interval-ℚ :
  closed-interval-ℚ → closed-interval-ℚ → Prop lzero
is-interior-prop-closed-interval-ℚ ((x , y) , _) ((x' , y') , _) =
  le-ℚ-Prop x x' ∧ le-ℚ-Prop y' y

is-interior-closed-interval-ℚ : closed-interval-ℚ → closed-interval-ℚ → UU lzero
is-interior-closed-interval-ℚ [x,y] [x',y'] =
  type-Prop (is-interior-prop-closed-interval-ℚ [x,y] [x',y'])

Recent changes