From 0f28249734cdc7bf0fe027387e7f29cd7c50fe00 Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Wed, 10 Dec 2025 16:40:51 -0800
Subject: [PATCH 1/2] Dense subsets of the real numbers

---
 .../dense-subsets-metric-spaces.lagda.md      |  18 +
 src/real-numbers.lagda.md                     |   2 +
 .../dense-subsets-real-numbers.lagda.md       | 416 ++++++++++++++++++
 .../metric-space-of-real-numbers.lagda.md     |  12 +
 ...onal-approximates-of-real-numbers.lagda.md |  93 ++++
 .../rational-real-numbers.lagda.md            |  45 +-
 6 files changed, 580 insertions(+), 6 deletions(-)
 create mode 100644 src/real-numbers/dense-subsets-real-numbers.lagda.md
 create mode 100644 src/real-numbers/rational-approximates-of-real-numbers.lagda.md

diff --git a/src/metric-spaces/dense-subsets-metric-spaces.lagda.md b/src/metric-spaces/dense-subsets-metric-spaces.lagda.md
index 307f1829908..02ba31f63ff 100644
--- a/src/metric-spaces/dense-subsets-metric-spaces.lagda.md
+++ b/src/metric-spaces/dense-subsets-metric-spaces.lagda.md
@@ -46,6 +46,24 @@ module _
 
   is-dense-subset-Metric-Space : UU (l1 ⊔ l2 ⊔ l3)
   is-dense-subset-Metric-Space = type-Prop is-dense-prop-subset-Metric-Space
+
+dense-subset-Metric-Space :
+  {l1 l2 : Level} (l3 : Level) (X : Metric-Space l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l3)
+dense-subset-Metric-Space l3 X =
+  type-subtype (is-dense-prop-subset-Metric-Space {l3 = l3} X)
+
+module _
+  {l1 l2 l3 : Level}
+  (X : Metric-Space l1 l2)
+  (S : dense-subset-Metric-Space l3 X)
+  where
+
+  subset-dense-subset-Metric-Space : subset-Metric-Space l3 X
+  subset-dense-subset-Metric-Space = pr1 S
+
+  is-dense-subset-dense-subset-Metric-Space :
+    is-dense-subset-Metric-Space X subset-dense-subset-Metric-Space
+  is-dense-subset-dense-subset-Metric-Space = pr2 S
 ```
 
 ## Properties
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index 8210a60b2e8..bf267d70310 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -24,6 +24,7 @@ open import real-numbers.cauchy-completeness-dedekind-real-numbers public
 open import real-numbers.cauchy-sequences-real-numbers public
 open import real-numbers.closed-intervals-real-numbers public
 open import real-numbers.dedekind-real-numbers public
+open import real-numbers.dense-subsets-real-numbers public
 open import real-numbers.difference-real-numbers public
 open import real-numbers.distance-real-numbers public
 open import real-numbers.enclosing-closed-rational-intervals-real-numbers public
@@ -87,6 +88,7 @@ open import real-numbers.positive-real-numbers public
 open import real-numbers.powers-real-numbers public
 open import real-numbers.proper-closed-intervals-real-numbers public
 open import real-numbers.raising-universe-levels-real-numbers public
+open import real-numbers.rational-approximates-of-real-numbers public
 open import real-numbers.rational-lower-dedekind-real-numbers public
 open import real-numbers.rational-real-numbers public
 open import real-numbers.rational-upper-dedekind-real-numbers public
diff --git a/src/real-numbers/dense-subsets-real-numbers.lagda.md b/src/real-numbers/dense-subsets-real-numbers.lagda.md
new file mode 100644
index 00000000000..e79e7552ca6
--- /dev/null
+++ b/src/real-numbers/dense-subsets-real-numbers.lagda.md
@@ -0,0 +1,416 @@
+# Dense subsets of the real numbers
+
+```agda
+module real-numbers.dense-subsets-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.minimum-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.intersections-subtypes
+open import foundation.propositional-truncations
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import logic.functoriality-existential-quantification
+
+open import metric-spaces.dense-subsets-metric-spaces
+
+open import order-theory.large-posets
+
+open import real-numbers.addition-positive-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.inequalities-addition-and-subtraction-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-approximates-of-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+open import real-numbers.subsets-real-numbers
+```
+
+</details>
+
+## Idea
+
+A {{#concept "dense subset" Disambiguation="of ℝ" Agda=dense-subset-ℝ}} of the
+[real numbers](real-numbers.dedekind-real-numbers.md) `ℝ` is a
+[dense subset](metric-spaces.dense-subsets-metric-spaces.md) of the
+[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md),
+which means that it is a [subset](real-numbers.subsets-real-numbers.md) `S ⊆ ℝ`
+such that for any `x : ℝ` and any
+[positive rational](elementary-number-theory.positive-rational-numbers.md) `ε`,
+there is a `y` in an `ε`-neighborhood of `X` that is also in `S`.
+
+## Definition
+
+```agda
+is-dense-subset-ℝ : {l1 l2 : Level} → subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2)
+is-dense-subset-ℝ = is-dense-subset-Metric-Space (metric-space-ℝ _)
+
+dense-subset-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+dense-subset-ℝ l1 l2 = dense-subset-Metric-Space l1 (metric-space-ℝ l2)
+
+subset-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → subset-ℝ l1 l2
+subset-dense-subset-ℝ = pr1
+
+is-dense-subset-dense-subset-ℝ :
+  {l1 l2 : Level} (S : dense-subset-ℝ l1 l2) (x : ℝ l2) (ε : ℚ⁺) →
+  intersect-subtype (neighborhood-prop-ℝ l2 ε x) (subset-dense-subset-ℝ S)
+is-dense-subset-dense-subset-ℝ = pr2
+
+type-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2)
+type-dense-subset-ℝ S = type-subtype (subset-dense-subset-ℝ S)
+
+inclusion-dense-subset-ℝ :
+  {l1 l2 : Level} (S : dense-subset-ℝ l1 l2) →
+  type-dense-subset-ℝ S → ℝ l2
+inclusion-dense-subset-ℝ S = inclusion-subtype (subset-dense-subset-ℝ S)
+
+is-in-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → ℝ l2 → UU l1
+is-in-dense-subset-ℝ S =
+  is-in-subtype (subset-dense-subset-ℝ S)
+```
+
+## Properties
+
+### The rational reals are dense in `ℝ`
+
+```agda
+abstract
+  is-dense-rational-real-ℝ :
+    (l : Level) → is-dense-subset-ℝ (subtype-rational-real {l})
+  is-dense-rational-real-ℝ l x ε =
+    map-exists
+      ( _)
+      ( raise-real-ℚ l)
+      ( λ q Nεxq → ( Nεxq , q , is-rational-raise-real-ℚ l q))
+      ( exists-rational-approximate-ℝ x ε)
+
+dense-subset-rational-real-ℝ :
+  (l : Level) → dense-subset-ℝ l l
+dense-subset-rational-real-ℝ l =
+  ( subtype-rational-real , is-dense-rational-real-ℝ l)
+```
+
+### Given a dense subset `S ⊆ R`, two reals `x < y`, and positive rationals `δx`, `δy`, there are `x' < y'` with `x' ∈ S`, `y' ∈ S`, `x'` in a `δx`-neighborhood of `x` and correspondingly for `y`
+
+```agda
+module _
+  {l1 l2 : Level}
+  (S : dense-subset-ℝ l1 l2)
+  where
+
+  abstract
+    exist-close-le-elements-dense-subset-ℝ :
+      {x y : ℝ l2} (δx δy : ℚ⁺) → le-ℝ x y →
+      exists
+        ( type-dense-subset-ℝ S × type-dense-subset-ℝ S)
+        ( λ ((x' , x'∈S) , (y' , y'∈S)) →
+          ( le-prop-ℝ x' y') ∧
+          ( neighborhood-prop-ℝ l2 δx x x') ∧
+          ( neighborhood-prop-ℝ l2 δy y y'))
+    exist-close-le-elements-dense-subset-ℝ {x} {y} δx δy x<y =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( ∃
+              ( type-dense-subset-ℝ S × type-dense-subset-ℝ S)
+              ( λ ((x' , x'∈S) , (y' , y'∈S)) →
+                ( le-prop-ℝ x' y') ∧
+                ( neighborhood-prop-ℝ l2 δx x x') ∧
+                ( neighborhood-prop-ℝ l2 δy y y')))
+      in do
+        (ε , x+ε<y) ← exists-positive-rational-separation-le-ℝ x<y
+        let (εx , εy , εx+εy=ε) = split-ℚ⁺ ε
+        (x' , Nxx' , x'∈S) ←
+          is-dense-subset-dense-subset-ℝ S x (min-ℚ⁺ δx εx)
+        (y' , Nyy' , y'∈S) ←
+          is-dense-subset-dense-subset-ℝ S y (min-ℚ⁺ δy εy)
+        intro-exists
+          ( (x' , x'∈S) , (y' , y'∈S))
+          ( concatenate-leq-le-ℝ
+              ( x')
+              ( x +ℝ real-ℚ⁺ εx)
+              ( y')
+              ( right-leq-real-bound-neighborhood-ℝ
+                ( εx)
+                ( x)
+                ( x')
+                ( weakly-monotonic-neighborhood-ℝ
+                  ( x)
+                  ( x')
+                  ( min-ℚ⁺ δx εx)
+                  ( εx)
+                  ( leq-right-min-ℚ⁺ δx εx)
+                  ( Nxx')))
+              ( concatenate-le-leq-ℝ
+                ( x +ℝ real-ℚ⁺ εx)
+                ( y -ℝ real-ℚ⁺ εy)
+                ( y')
+                ( le-transpose-left-add-ℝ
+                  ( x +ℝ real-ℚ⁺ εx)
+                  ( real-ℚ⁺ εy)
+                  ( y)
+                  ( inv-tr
+                    ( λ z → le-ℝ z y)
+                    ( ( associative-add-ℝ _ _ _) ∙
+                      ( ap-add-ℝ
+                        ( refl)
+                        ( ( add-real-ℚ _ _ ∙ ap real-ℚ⁺ εx+εy=ε))))
+                    ( x+ε<y)))
+                ( leq-transpose-right-add-ℝ
+                  ( y)
+                  ( y')
+                  ( real-ℚ⁺ εy)
+                  ( left-leq-real-bound-neighborhood-ℝ
+                    ( εy)
+                    ( y)
+                    ( y')
+                    ( weakly-monotonic-neighborhood-ℝ
+                      ( y)
+                      ( y')
+                      ( min-ℚ⁺ δy εy)
+                      ( εy)
+                      ( leq-right-min-ℚ⁺ δy εy)
+                      ( Nyy'))))) ,
+            weakly-monotonic-neighborhood-ℝ
+              ( x)
+              ( x')
+              ( min-ℚ⁺ δx εx)
+              ( δx)
+              ( leq-left-min-ℚ⁺ δx εx)
+              ( Nxx') ,
+            weakly-monotonic-neighborhood-ℝ
+              ( y)
+              ( y')
+              ( min-ℚ⁺ δy εy)
+              ( δy)
+              ( leq-left-min-ℚ⁺ δy εy)
+              ( Nyy'))
+```
+
+### Given a dense subset `S ⊆ ℝ`, for any `x : ℝ` and `ε : ℚ⁺` there is an element of `S` in an `ε`-neighborhood of `x` that is greater than or equal to `x`
+
+```agda
+module _
+  {l1 l2 : Level}
+  (S : dense-subset-ℝ l1 l2)
+  (x : ℝ l2)
+  where
+
+  abstract
+    is-dense-above-dense-subset-ℝ :
+      (ε : ℚ⁺) →
+      exists
+        ( ℝ l2)
+        ( λ y →
+          ( leq-prop-ℝ x y) ∧
+          ( subset-dense-subset-ℝ S y) ∧
+          ( neighborhood-prop-ℝ l2 ε x y))
+    is-dense-above-dense-subset-ℝ ε =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+        open
+          do-syntax-trunc-Prop
+            ( ∃
+              ( ℝ l2)
+              ( λ y →
+                ( leq-prop-ℝ x y) ∧
+                ( subset-dense-subset-ℝ S y) ∧
+                ( neighborhood-prop-ℝ l2 ε x y)))
+      in do
+        (ε' , 2ε'<ε) ← double-le-ℚ⁺ ε
+        (y , N , y∈S) ←
+          is-dense-subset-dense-subset-ℝ S (x +ℝ real-ℚ⁺ ε') ε'
+        let
+          x≤y : leq-ℝ x y
+          x≤y =
+            reflects-leq-right-add-ℝ
+              ( real-ℚ⁺ ε')
+              ( x)
+              ( y)
+              ( left-leq-real-bound-neighborhood-ℝ ε' (x +ℝ real-ℚ⁺ ε') y N)
+        intro-exists
+          ( y)
+          ( x≤y ,
+            y∈S ,
+            neighborhood-real-bound-each-leq-ℝ
+              ( ε)
+              ( x)
+              ( y)
+              ( chain-of-inequalities
+                x
+                ≤ y
+                  by x≤y
+                ≤ y +ℝ real-ℚ⁺ ε
+                  by leq-left-add-real-ℝ⁺ y (positive-real-ℚ⁺ ε))
+              ( chain-of-inequalities
+                y
+                ≤ (x +ℝ real-ℚ⁺ ε') +ℝ real-ℚ⁺ ε'
+                  by right-leq-real-bound-neighborhood-ℝ ε' _ _ N
+                ≤ x +ℝ (real-ℚ⁺ ε' +ℝ real-ℚ⁺ ε')
+                  by leq-eq-ℝ (associative-add-ℝ _ _ _)
+                ≤ x +ℝ real-ℚ⁺ (ε' +ℚ⁺ ε')
+                  by leq-eq-ℝ (ap-add-ℝ refl (add-real-ℚ _ _))
+                ≤ x +ℝ real-ℚ⁺ ε
+                  by
+                    preserves-leq-left-add-ℝ x _ _
+                      ( preserves-leq-real-ℚ (leq-le-ℚ 2ε'<ε))))
+```
+
+### Given a dense subset `S ⊆ ℝ`, for any `x : ℝ` and `ε : ℚ⁺` there is an element of `S` in an `ε`-neighborhood of `x` that is less than or equal to `x`
+
+```agda
+module _
+  {l1 l2 : Level}
+  (S : dense-subset-ℝ l1 l2)
+  (x : ℝ l2)
+  where
+
+  abstract
+    is-dense-below-dense-subset-ℝ :
+      (ε : ℚ⁺) →
+      exists
+        ( ℝ l2)
+        ( λ y →
+          ( leq-prop-ℝ y x) ∧
+          ( subset-dense-subset-ℝ S y) ∧
+          ( neighborhood-prop-ℝ l2 ε x y))
+    is-dense-below-dense-subset-ℝ ε =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+        open
+          do-syntax-trunc-Prop
+            ( ∃
+              ( ℝ l2)
+              ( λ y →
+                ( leq-prop-ℝ y x) ∧
+                ( subset-dense-subset-ℝ S y) ∧
+                ( neighborhood-prop-ℝ l2 ε x y)))
+      in do
+        (ε' , 2ε'<ε) ← double-le-ℚ⁺ ε
+        (y , N , y∈S) ←
+          is-dense-subset-dense-subset-ℝ S (x -ℝ real-ℚ⁺ ε') ε'
+        let
+          y≤x =
+            tr
+              ( leq-ℝ y)
+              ( eq-sim-ℝ (cancel-right-diff-add-ℝ x (real-ℚ⁺ ε')))
+              ( right-leq-real-bound-neighborhood-ℝ ε' _ _ N)
+        intro-exists
+          ( y)
+          ( y≤x ,
+            y∈S ,
+            neighborhood-real-bound-each-leq-ℝ
+              ( ε)
+              ( x)
+              ( y)
+              ( chain-of-inequalities
+                x
+                ≤ (x -ℝ real-ℚ⁺ ε') +ℝ real-ℚ⁺ ε'
+                  by
+                    leq-sim-ℝ
+                      ( symmetric-sim-ℝ
+                        ( cancel-right-diff-add-ℝ x (real-ℚ⁺ ε')))
+                ≤ (y +ℝ real-ℚ⁺ ε') +ℝ real-ℚ⁺ ε'
+                  by
+                    preserves-leq-right-add-ℝ
+                      ( real-ℚ⁺ ε')
+                      ( x -ℝ real-ℚ⁺ ε')
+                      ( y +ℝ real-ℚ⁺ ε')
+                      ( left-leq-real-bound-neighborhood-ℝ ε' _ _ N)
+                ≤ y +ℝ (real-ℚ⁺ ε' +ℝ real-ℚ⁺ ε')
+                  by leq-eq-ℝ (associative-add-ℝ _ _ _)
+                ≤ y +ℝ real-ℚ⁺ (ε' +ℚ⁺ ε')
+                  by leq-eq-ℝ (ap-add-ℝ refl (add-real-ℚ _ _))
+                ≤ y +ℝ real-ℚ⁺ ε
+                  by
+                    preserves-leq-left-add-ℝ
+                      ( y)
+                      ( _)
+                      ( _)
+                      ( preserves-leq-real-ℚ (leq-le-ℚ 2ε'<ε)))
+              ( chain-of-inequalities
+                y
+                ≤ x
+                  by y≤x
+                ≤ x +ℝ real-ℚ⁺ ε
+                  by leq-left-add-real-ℝ⁺ x (positive-real-ℚ⁺ ε)))
+```
+
+### If `S` is dense in `ℝ` and `x < y`, then there is an `s ∈ S` with `x < s < y`
+
+```agda
+module _
+  {l1 l2 : Level}
+  (S : dense-subset-ℝ l1 l2)
+  {x y : ℝ l2}
+  (x<y : le-ℝ x y)
+  where
+
+  abstract
+    dense-le-dense-subset-ℝ :
+      exists
+        ( ℝ l2)
+        ( λ s → subset-dense-subset-ℝ S s ∧ le-prop-ℝ x s ∧ le-prop-ℝ s y)
+    dense-le-dense-subset-ℝ =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+        open
+          do-syntax-trunc-Prop
+            ( ∃
+              ( ℝ l2)
+              ( λ s →
+                subset-dense-subset-ℝ S s ∧ le-prop-ℝ x s ∧ le-prop-ℝ s y))
+      in do
+        (a , x<a , a<y) ← dense-le-ℝ x y x<y
+        (b , a<b , b<y) ← dense-le-ℝ a y a<y
+        (ε , a+ε<b) ← exists-positive-rational-separation-le-ℝ a<b
+        (c , a≤c , c∈S , Nεac) ←
+          is-dense-above-dense-subset-ℝ S (raise-ℝ l2 a) ε
+        intro-exists
+          ( c)
+          ( c∈S ,
+            concatenate-le-leq-ℝ
+              ( x)
+              ( a)
+              ( c)
+              ( x<a)
+              ( preserves-leq-left-sim-ℝ (sim-raise-ℝ' l2 a) a≤c) ,
+            concatenate-leq-le-ℝ
+              ( c)
+              ( b)
+              ( y)
+              ( chain-of-inequalities
+                c
+                ≤ raise-ℝ l2 a +ℝ real-ℚ⁺ ε
+                  by right-leq-real-bound-neighborhood-ℝ ε _ _ Nεac
+                ≤ a +ℝ real-ℚ⁺ ε
+                  by
+                    preserves-leq-right-add-ℝ _ _ _
+                      ( leq-sim-ℝ (sim-raise-ℝ' l2 a))
+                ≤ b
+                  by leq-le-ℝ a+ε<b)
+              ( b<y))
+```
diff --git a/src/real-numbers/metric-space-of-real-numbers.lagda.md b/src/real-numbers/metric-space-of-real-numbers.lagda.md
index a5f9e1bc435..21e16b10ec5 100644
--- a/src/real-numbers/metric-space-of-real-numbers.lagda.md
+++ b/src/real-numbers/metric-space-of-real-numbers.lagda.md
@@ -12,6 +12,7 @@ module real-numbers.metric-space-of-real-numbers where
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.inequality-positive-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 
@@ -386,6 +387,17 @@ module _
         ( right-leq-real-bound-neighborhood-ℝ d x y H))
 ```
 
+### The neighborhood relation on the real numbers is weakly monotonic
+
+```agda
+abstract
+  weakly-monotonic-neighborhood-ℝ :
+    {l : Level} (x y : ℝ l) (d₁ d₂ : ℚ⁺) → leq-ℚ⁺ d₁ d₂ →
+    neighborhood-ℝ l d₁ x y → neighborhood-ℝ l d₂ x y
+  weakly-monotonic-neighborhood-ℝ {l} =
+    weakly-monotonic-neighborhood-Metric-Space (metric-space-ℝ l)
+```
+
 ### The canonical embedding from rational to real numbers is an isometry between metric spaces
 
 ```agda
diff --git a/src/real-numbers/rational-approximates-of-real-numbers.lagda.md b/src/real-numbers/rational-approximates-of-real-numbers.lagda.md
new file mode 100644
index 00000000000..917c15d716e
--- /dev/null
+++ b/src/real-numbers/rational-approximates-of-real-numbers.lagda.md
@@ -0,0 +1,93 @@
+# Rational approximates of real numbers
+
+```agda
+module real-numbers.rational-approximates-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.propositional-truncations
+open import foundation.raising-universe-levels
+open import foundation.universe-levels
+
+open import metric-spaces.dense-subsets-metric-spaces
+
+open import real-numbers.arithmetically-located-dedekind-cuts
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.rational-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "rational approximate" Disambiguation="of a real number" Agda=rational-approximate-ℝ}}
+of a [real number](real-numbers.dedekind-real-numbers.md) `x` to some
+[positive rational](elementary-number-theory.positive-rational-numbers.md) `ε`
+is a [rational number](elementary-number-theory.rational-numbers.md) whose
+[canonical embedding](real-numbers.rational-real-numbers.md) in the real numbers
+is within an `ε`-neighborhood of `x` in the
+[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md).
+
+## Definition
+
+```agda
+rational-approximate-ℝ : {l : Level} → ℝ l → ℚ⁺ → UU l
+rational-approximate-ℝ {l} x ε =
+  Σ ℚ (λ q → neighborhood-ℝ l ε x (raise-real-ℚ l q))
+```
+
+## Properties
+
+### Any real number can be approximated to any positive rational `ε`
+
+```agda
+abstract opaque
+  unfolding neighborhood-ℝ real-ℚ
+
+  exists-rational-approximate-ℝ :
+    {l : Level} (x : ℝ l) (ε : ℚ⁺) →
+    exists ℚ (λ q → neighborhood-prop-ℝ l ε x (raise-real-ℚ l q))
+  exists-rational-approximate-ℝ {l} x ε⁺@(ε , _) =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( ∃ ℚ (λ q → neighborhood-prop-ℝ l ε⁺ x (raise-real-ℚ l q)))
+    in do
+      ((p , q) , q<p+ε , p<x , x<q) ← is-arithmetically-located-ℝ x ε⁺
+      intro-exists
+        ( p)
+        ( ( λ r r+ε<p →
+            le-lower-cut-ℝ
+              ( x)
+              ( transitive-le-ℚ
+                ( r)
+                ( r +ℚ ε)
+                ( p)
+                ( map-inv-raise r+ε<p)
+                ( le-right-add-rational-ℚ⁺ r ε⁺))
+              ( p<x)) ,
+          ( λ r r+ε<x →
+            map-raise
+              ( reflects-le-left-add-ℚ
+                ( ε)
+                ( r)
+                ( p)
+                ( transitive-le-ℚ
+                  ( r +ℚ ε)
+                  ( q)
+                  ( p +ℚ ε)
+                  ( q<p+ε)
+                  ( le-lower-upper-cut-ℝ x r+ε<x x<q)))))
+```
diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md
index 3a435d07231..b72d292874f 100644
--- a/src/real-numbers/rational-real-numbers.lagda.md
+++ b/src/real-numbers/rational-real-numbers.lagda.md
@@ -28,6 +28,7 @@ open import foundation.injective-maps
 open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositions
+open import foundation.raising-universe-levels
 open import foundation.retractions
 open import foundation.sections
 open import foundation.subtypes
@@ -208,17 +209,33 @@ module _
 ### The real embedding of a rational number is rational
 
 ```agda
-opaque
+abstract opaque
   unfolding real-ℚ
 
   is-rational-real-ℚ : (p : ℚ) → is-rational-ℝ (real-ℚ p) p
   is-rational-real-ℚ p = (irreflexive-le-ℚ p , irreflexive-le-ℚ p)
 ```
 
+### A rational real number raised to another universe level is rational
+
+```agda
+abstract
+  is-rational-raise-ℝ :
+    {l0 : Level} (l : Level) (x : ℝ l0) {q : ℚ} →
+    is-rational-ℝ x q → is-rational-ℝ (raise-ℝ l x) q
+  is-rational-raise-ℝ l x (q≮x , x≮q) =
+    ( q≮x ∘ map-inv-raise , x≮q ∘ map-inv-raise)
+
+  is-rational-raise-real-ℚ :
+    (l : Level) (p : ℚ) → is-rational-ℝ (raise-real-ℚ l p) p
+  is-rational-raise-real-ℚ l p =
+    is-rational-raise-ℝ l (real-ℚ p) (is-rational-real-ℚ p)
+```
+
 ### Rational real numbers are embedded rationals
 
 ```agda
-opaque
+abstract opaque
   unfolding real-ℚ sim-ℝ
 
   sim-rational-ℝ :
@@ -239,10 +256,22 @@ opaque
       ( ex-falso ∘ q∉ux)
       ( is-located-lower-upper-cut-ℝ x p<q)
 
-eq-real-rational-is-rational-ℝ :
-  (x : ℝ lzero) (q : ℚ) (H : is-rational-ℝ x q) → real-ℚ q ＝ x
-eq-real-rational-is-rational-ℝ x q H =
-  inv (eq-sim-ℝ {lzero} {x} {real-ℚ q} (sim-rational-ℝ (x , q , H)))
+abstract
+  eq-real-rational-is-rational-ℝ :
+    (x : ℝ lzero) (q : ℚ) (H : is-rational-ℝ x q) → real-ℚ q ＝ x
+  eq-real-rational-is-rational-ℝ x q H =
+    inv (eq-sim-ℝ {lzero} {x} {real-ℚ q} (sim-rational-ℝ (x , q , H)))
+
+  eq-raise-real-rational-is-rational-ℝ :
+    {l : Level} (x : ℝ l) (q : ℚ) → is-rational-ℝ x q → x ＝ raise-real-ℚ l q
+  eq-raise-real-rational-is-rational-ℝ {l} x q H =
+    eq-sim-ℝ
+      ( transitive-sim-ℝ
+        ( x)
+        ( real-ℚ q)
+        ( raise-real-ℚ l q)
+        ( sim-raise-ℝ l (real-ℚ q))
+        ( sim-rational-ℝ (x , q , H)))
 ```
 
 ### The canonical map from rationals to rational reals
@@ -250,6 +279,10 @@ eq-real-rational-is-rational-ℝ x q H =
 ```agda
 rational-real-ℚ : ℚ → Rational-ℝ lzero
 rational-real-ℚ q = (real-ℚ q , q , is-rational-real-ℚ q)
+
+raise-rational-real-ℚ : (l : Level) → ℚ → Rational-ℝ l
+raise-rational-real-ℚ l q =
+  ( raise-real-ℚ l q , q , is-rational-raise-real-ℚ l q)
 ```
 
 ### The rationals and rational reals are equivalent

From 8e6cf9aeb739d01bdef837cbb1aa341b8806e1ea Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Thu, 11 Dec 2025 09:28:24 -0800
Subject: [PATCH 2/2] Update
 src/real-numbers/dense-subsets-real-numbers.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/real-numbers/dense-subsets-real-numbers.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/real-numbers/dense-subsets-real-numbers.lagda.md b/src/real-numbers/dense-subsets-real-numbers.lagda.md
index e79e7552ca6..8245529a68f 100644
--- a/src/real-numbers/dense-subsets-real-numbers.lagda.md
+++ b/src/real-numbers/dense-subsets-real-numbers.lagda.md
@@ -104,7 +104,7 @@ abstract
     map-exists
       ( _)
       ( raise-real-ℚ l)
-      ( λ q Nεxq → ( Nεxq , q , is-rational-raise-real-ℚ l q))
+      ( λ q Nεxq → (Nεxq , q , is-rational-raise-real-ℚ l q))
       ( exists-rational-approximate-ℝ x ε)
 
 dense-subset-rational-real-ℝ :