Positive closed intervals in the rational numbers

Content created by Louis Wasserman.

Created on 2025-11-26.
Last modified on 2025-11-26.

module elementary-number-theory.positive-closed-intervals-rational-numbers where
Imports 
open import elementary-number-theory.closed-intervals-rational-numbers
open import elementary-number-theory.positive-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 positive if every element in it is positive, or equivalently, its lower bound is positive.

Definition

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

is-positive-closed-interval-ℚ : closed-interval-ℚ → UU lzero
is-positive-closed-interval-ℚ ((a , b) , _) = is-positive-ℚ a

abstract
  is-positive-upper-bound-is-positive-closed-interval-ℚ :
    ([a,b] : closed-interval-ℚ) → is-positive-closed-interval-ℚ [a,b] →
    is-positive-ℚ (upper-bound-closed-interval-ℚ [a,b])
  is-positive-upper-bound-is-positive-closed-interval-ℚ ((a , b) , a≤b) pos-a =
    is-positive-leq-ℚ⁺ (a , pos-a) a≤b

Recent changes