Similarity of positive real numbers

Content created by Louis Wasserman.

Created on 2025-11-09.
Last modified on 2025-11-09.

module real-numbers.similarity-positive-real-numbers where
Imports 
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

open import real-numbers.positive-real-numbers
open import real-numbers.similarity-real-numbers

Idea

Two positive real numbers are similar if they are similar as real numbers.

Definition

sim-prop-ℝ⁺ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁺ l2 → Prop (l1 ⊔ l2)
sim-prop-ℝ⁺ (x , _) (y , _) = sim-prop-ℝ x y

sim-ℝ⁺ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁺ l2 → UU (l1 ⊔ l2)
sim-ℝ⁺ (x , _) (y , _) = sim-ℝ x y

Recent changes