Strict inequality on nonnegative rational numbers

Content created by Louis Wasserman.

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

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

Strict inequality on the nonnegative rational numbers is transitive

abstract
  transitive-le-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → le-ℚ⁰⁺ q r → le-ℚ⁰⁺ p q → le-ℚ⁰⁺ p r
  transitive-le-ℚ⁰⁺ (p , _) (q , _) (r , _) = transitive-le-ℚ p q r

Concatenation laws with inequality

abstract
  concatenate-le-leq-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → le-ℚ⁰⁺ p q → leq-ℚ⁰⁺ q r → le-ℚ⁰⁺ p r
  concatenate-le-leq-ℚ⁰⁺ (p , _) (q , _) (r , _) = concatenate-le-leq-ℚ p q r

  concatenate-leq-le-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → leq-ℚ⁰⁺ p q → le-ℚ⁰⁺ q r → le-ℚ⁰⁺ p r
  concatenate-leq-le-ℚ⁰⁺ (p , _) (q , _) (r , _) = concatenate-leq-le-ℚ p q r

Recent changes