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

Definition

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

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

abstract
  is-negative-lower-bound-is-negative-closed-interval-ℚ :
    ([a,b] : closed-interval-ℚ) → is-negative-closed-interval-ℚ [a,b] →
    is-negative-ℚ (lower-bound-closed-interval-ℚ [a,b])
  is-negative-lower-bound-is-negative-closed-interval-ℚ ((a , b) , a≤b) neg-b =
    is-negative-leq-ℚ⁻ (b , neg-b) a≤b

Recent changes