Strict 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.strict-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.positive-real-numbers
open import real-numbers.strict-inequality-real-numbers

Idea

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

Definition

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

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

Recent changes