Strict inequality on nonnegative rational numbers

Content created by Louis Wasserman.

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

module elementary-number-theory.strict-inequality-nonnegative-rational-numbers where
Imports 
open import elementary-number-theory.nonnegative-rational-numbers
open import elementary-number-theory.positive-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

The standard strict ordering on the nonnegative rational numbers is inherited from the standard strict ordering on rational numbers.

Definition

le-prop-ℚ⁰⁺ : (p q : ℚ⁰⁺) → Prop lzero
le-prop-ℚ⁰⁺ p q = le-ℚ-Prop (rational-ℚ⁰⁺ p) (rational-ℚ⁰⁺ q)

le-ℚ⁰⁺ : (p q : ℚ⁰⁺) → UU lzero
le-ℚ⁰⁺ p q = type-Prop (le-prop-ℚ⁰⁺ p q)

Properties

Zero is less than positive rational numbers as nonnegative rational numbers

abstract
  le-zero-nonnegative-ℚ⁰⁺ : (q : ℚ⁺) → le-ℚ⁰⁺ zero-ℚ⁰⁺ (nonnegative-ℚ⁺ q)
  le-zero-nonnegative-ℚ⁰⁺ (q , pos-q) = le-zero-is-positive-ℚ q pos-q

Recent changes