The metric space of nonnegative real numbers

Content created by Louis Wasserman.

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

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

module real-numbers.metric-space-of-nonnegative-real-numbers where
Imports 
open import foundation.universe-levels

open import metric-spaces.metric-spaces

open import real-numbers.nonnegative-real-numbers
open import real-numbers.subsets-real-numbers

Idea

The nonnegative real numbers form a subspace of the metric space of real numbers.

Definition

metric-space-ℝ⁰⁺ : (l : Level) → Metric-Space (lsuc l) l
metric-space-ℝ⁰⁺ l = metric-space-subset-ℝ (is-nonnegative-prop-ℝ {l})

Recent changes