Inequality on the nonnegative rational numbers

Content created by Louis Wasserman.

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

module elementary-number-theory.inequality-nonnegative-rational-numbers where
Imports 
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.nonnegative-rational-numbers

open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

Idea

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

Definition

leq-prop-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → Prop lzero
leq-prop-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ-Prop p q

leq-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → UU lzero
leq-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ p q

Recent changes