Inequality of positive real numbers

Content created by Louis Wasserman.

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

{-# OPTIONS --lossy-unification #-}

module real-numbers.inequality-positive-real-numbers where
Imports 
open import foundation.propositions
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.positive-real-numbers

Idea

The standard ordering on the positive real numbers is inherited from the standard ordering on real numbers.

Definition

leq-prop-ℝ⁺ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁺ l2 → Prop (l1 ⊔ l2)
leq-prop-ℝ⁺ x y = leq-prop-ℝ (real-ℝ⁺ x) (real-ℝ⁺ y)

leq-ℝ⁺ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁺ l2 → UU (l1 ⊔ l2)
leq-ℝ⁺ x y = type-Prop (leq-prop-ℝ⁺ x y)

Recent changes