diff --git a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md
index e496147954..fd1909ddec 100644
--- a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md
@@ -453,11 +453,12 @@ module _
           ( left-summand-split-ℚ⁺ p)
           ( right-summand-split-ℚ⁺ p))
 
-    bound-double-le-ℚ⁺ :
-      Σ ℚ⁺ (λ q → le-ℚ⁺ (q +ℚ⁺ q) p)
-    bound-double-le-ℚ⁺ =
-      ( modulus-le-double-le-ℚ⁺ , le-double-le-modulus-le-double-le-ℚ⁺)
+  bound-double-le-ℚ⁺ :
+    Σ ℚ⁺ (λ q → le-ℚ⁺ (q +ℚ⁺ q) p)
+  bound-double-le-ℚ⁺ =
+    ( modulus-le-double-le-ℚ⁺ , le-double-le-modulus-le-double-le-ℚ⁺)
 
+  abstract
     double-le-ℚ⁺ : exists ℚ⁺ (λ q → le-prop-ℚ⁺ (q +ℚ⁺ q) p)
     double-le-ℚ⁺ = unit-trunc-Prop bound-double-le-ℚ⁺
 ```
diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index d08a6ffd1f..bc48c2ee7e 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -56,6 +56,7 @@ metric space, `N d₂ x y` [or](foundation.disjunction.md)
 ```agda
 module metric-spaces where
 
+open import metric-spaces.accumulation-points-subsets-located-metric-spaces public
 open import metric-spaces.apartness-located-metric-spaces public
 open import metric-spaces.approximations-located-metric-spaces public
 open import metric-spaces.approximations-metric-spaces public
diff --git a/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md b/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md
new file mode 100644
index 0000000000..8f84ddb509
--- /dev/null
+++ b/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md
@@ -0,0 +1,319 @@
+# Accumulation points of subsets of located metric spaces
+
+```agda
+module metric-spaces.accumulation-points-subsets-located-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.intersections-subtypes
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import lists.sequences
+
+open import logic.functoriality-existential-quantification
+
+open import metric-spaces.apartness-located-metric-spaces
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.cauchy-sequences-metric-spaces
+open import metric-spaces.closed-subsets-located-metric-spaces
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
+open import metric-spaces.limits-of-sequences-metric-spaces
+open import metric-spaces.located-metric-spaces
+open import metric-spaces.subspaces-metric-spaces
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "accumulation point" WDID=Q858223 WD="limit point" Disambiguation="of a subset of a located metric space" Agda=accumulation-point-subset-Located-Metric-Space}}
+of a subset `S` of a
+[located metric space](metric-spaces.located-metric-spaces.md) `X` is a point
+`x : X` such that there exists a
+[Cauchy approximation](metric-spaces.cauchy-approximations-metric-spaces.md) `a`
+with [limit](metric-spaces.limits-of-cauchy-approximations-metric-spaces.md) `x`
+such that for every `ε : ℚ⁺`, `a ε` is in `S` and is
+[apart](metric-spaces.apartness-located-metric-spaces.md) from `x`. In
+particular, this implies an accumulation point is not isolated.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (X : Located-Metric-Space l1 l2)
+  (S : subset-Located-Metric-Space l3 X)
+  where
+
+  is-accumulation-to-point-prop-subset-Located-Metric-Space :
+    type-Located-Metric-Space X →
+    subtype
+      ( l2)
+      ( cauchy-approximation-Metric-Space (subspace-Located-Metric-Space X S))
+  is-accumulation-to-point-prop-subset-Located-Metric-Space x a =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ ε →
+        apart-prop-Located-Metric-Space X
+          ( pr1
+            ( map-cauchy-approximation-Metric-Space
+              ( subspace-Located-Metric-Space X S)
+              ( a)
+              ( ε)))
+          ( x)) ∧
+    is-limit-cauchy-approximation-prop-Metric-Space
+      ( metric-space-Located-Metric-Space X)
+      ( map-short-function-cauchy-approximation-Metric-Space
+        ( subspace-Located-Metric-Space X S)
+        ( metric-space-Located-Metric-Space X)
+        ( short-inclusion-subspace-Metric-Space
+          ( metric-space-Located-Metric-Space X)
+          ( S))
+        ( a))
+      ( x)
+
+  is-accumulation-to-point-subset-Located-Metric-Space :
+    type-Located-Metric-Space X →
+    cauchy-approximation-Metric-Space (subspace-Located-Metric-Space X S) →
+    UU l2
+  is-accumulation-to-point-subset-Located-Metric-Space x a =
+    type-Prop (is-accumulation-to-point-prop-subset-Located-Metric-Space x a)
+
+  is-accumulation-point-prop-subset-Located-Metric-Space :
+    subset-Metric-Space (l1 ⊔ l2 ⊔ l3) (metric-space-Located-Metric-Space X)
+  is-accumulation-point-prop-subset-Located-Metric-Space x =
+    ∃ ( cauchy-approximation-Metric-Space (subspace-Located-Metric-Space X S))
+      ( is-accumulation-to-point-prop-subset-Located-Metric-Space x)
+
+  is-accumulation-point-subset-Located-Metric-Space :
+    type-Located-Metric-Space X → UU (l1 ⊔ l2 ⊔ l3)
+  is-accumulation-point-subset-Located-Metric-Space x =
+    type-Prop (is-accumulation-point-prop-subset-Located-Metric-Space x)
+
+  accumulation-point-subset-Located-Metric-Space : UU (l1 ⊔ l2 ⊔ l3)
+  accumulation-point-subset-Located-Metric-Space =
+    type-subtype is-accumulation-point-prop-subset-Located-Metric-Space
+```
+
+## Properties
+
+### A closed subset of a metric space contains all its accumulation points
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (X : Located-Metric-Space l1 l2)
+  (S : closed-subset-Located-Metric-Space l3 X)
+  where
+
+  is-in-closed-subset-is-accumulation-point-Located-Metric-Space :
+    (x : type-Located-Metric-Space X) →
+    is-accumulation-point-subset-Located-Metric-Space
+      ( X)
+      ( subset-closed-subset-Located-Metric-Space X S)
+      ( x) →
+    is-in-closed-subset-Located-Metric-Space X S x
+  is-in-closed-subset-is-accumulation-point-Located-Metric-Space x is-acc-x =
+    is-closed-subset-closed-subset-Located-Metric-Space
+      ( X)
+      ( S)
+      ( x)
+      ( λ ε →
+        let
+          open
+            do-syntax-trunc-Prop
+              ( ∃
+                ( type-Located-Metric-Space X)
+                ( λ y →
+                  neighborhood-prop-Located-Metric-Space X ε x y ∧
+                  subset-closed-subset-Located-Metric-Space X S y))
+        in do
+          (approx@(a , _) , a#x , lim-a=x) ← is-acc-x
+          let (y , y∈S) = a ε
+          intro-exists
+            ( y)
+            ( symmetric-neighborhood-Located-Metric-Space X
+              ( ε)
+              ( y)
+              ( x)
+              ( saturated-is-limit-cauchy-approximation-Metric-Space
+                ( metric-space-Located-Metric-Space X)
+                ( map-short-function-cauchy-approximation-Metric-Space
+                  ( subspace-Located-Metric-Space
+                    ( X)
+                    ( subset-closed-subset-Located-Metric-Space X S))
+                  ( metric-space-Located-Metric-Space X)
+                  ( short-inclusion-subspace-Metric-Space
+                    ( metric-space-Located-Metric-Space X)
+                    ( subset-closed-subset-Located-Metric-Space X S))
+                  ( approx))
+                ( x)
+                ( lim-a=x)
+                ( ε)) ,
+              y∈S))
+```
+
+### The property of being a sequential accumulation point
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (X : Located-Metric-Space l1 l2)
+  (S : subset-Located-Metric-Space l3 X)
+  (x : type-Located-Metric-Space X)
+  where
+
+  is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space :
+    subtype l2 (sequence (type-subtype S))
+  is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space a =
+    Π-Prop ℕ (λ n → apart-prop-Located-Metric-Space X (pr1 (a n)) x) ∧
+    is-limit-prop-sequence-Metric-Space
+      ( metric-space-Located-Metric-Space X)
+      ( pr1 ∘ a)
+      ( x)
+
+  is-sequence-accumulating-to-point-subset-Located-Metric-Space :
+    sequence (type-subtype S) → UU l2
+  is-sequence-accumulating-to-point-subset-Located-Metric-Space =
+    is-in-subtype
+      ( is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space)
+
+  is-sequential-accumulation-point-prop-subset-Located-Metric-Space :
+    Prop (l1 ⊔ l2 ⊔ l3)
+  is-sequential-accumulation-point-prop-subset-Located-Metric-Space =
+    ∃ ( sequence (type-subtype S))
+      ( is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space)
+
+  is-sequential-accumulation-point-subset-Located-Metric-Space :
+    UU (l1 ⊔ l2 ⊔ l3)
+  is-sequential-accumulation-point-subset-Located-Metric-Space =
+    type-Prop is-sequential-accumulation-point-prop-subset-Located-Metric-Space
+```
+
+### If `x` is an accumulation point of `S`, it is a sequential accumulation point of `S`
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (X : Located-Metric-Space l1 l2)
+  (S : subset-Located-Metric-Space l3 X)
+  (x : type-Located-Metric-Space X)
+  where
+
+  abstract
+    is-sequential-accumulation-point-is-accumulation-point-subset-Located-Metric-Space :
+      is-accumulation-point-subset-Located-Metric-Space X S x →
+      is-sequential-accumulation-point-subset-Located-Metric-Space X S x
+    is-sequential-accumulation-point-is-accumulation-point-subset-Located-Metric-Space =
+      map-exists
+        ( _)
+        ( map-cauchy-sequence-cauchy-approximation-Metric-Space
+          ( subspace-Located-Metric-Space X S))
+        ( λ a (a#x , lim-a=x) →
+          ( ( λ n → a#x _) ,
+            is-limit-cauchy-sequence-cauchy-approximation-Metric-Space
+              ( metric-space-Located-Metric-Space X)
+              ( map-short-function-cauchy-approximation-Metric-Space
+                ( subspace-Located-Metric-Space X S)
+                ( metric-space-Located-Metric-Space X)
+                ( short-inclusion-subspace-Metric-Space
+                  ( metric-space-Located-Metric-Space X)
+                  ( S))
+                ( a))
+              ( x)
+              ( lim-a=x)))
+```
+
+### If `x` is a sequential accumulation point of `S`, it is an accumulation point of `S`
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (X : Located-Metric-Space l1 l2)
+  (S : subset-Located-Metric-Space l3 X)
+  (x : type-Located-Metric-Space X)
+  where
+
+  abstract
+    is-accumulation-point-is-sequential-accumulation-point-subset-Located-Metric-Space :
+      is-sequential-accumulation-point-subset-Located-Metric-Space X S x →
+      is-accumulation-point-subset-Located-Metric-Space X S x
+    is-accumulation-point-is-sequential-accumulation-point-subset-Located-Metric-Space
+      is-seq-acc-x =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( is-accumulation-point-prop-subset-Located-Metric-Space X S x)
+      in do
+        (σ , σ#x , lim-σ=x) ← is-seq-acc-x
+        μ@(mod-μ , is-mod-μ) ← lim-σ=x
+        intro-exists
+          ( cauchy-approximation-cauchy-sequence-Metric-Space
+            ( subspace-Located-Metric-Space X S)
+            ( σ ,
+              is-cauchy-has-limit-modulus-sequence-Metric-Space
+                ( metric-space-Located-Metric-Space X)
+                ( pr1 ∘ σ)
+                ( x)
+                ( μ)))
+          ( ( λ ε → σ#x _) ,
+            ( λ ε δ →
+              let ε' = modulus-le-double-le-ℚ⁺ ε
+              in
+                monotonic-neighborhood-Located-Metric-Space
+                  ( X)
+                  ( pr1 (σ (mod-μ ε')))
+                  ( x)
+                  ( ε')
+                  ( ε +ℚ⁺ δ)
+                  ( transitive-le-ℚ _ _ _
+                    ( le-left-add-ℚ⁺ ε δ)
+                    ( le-modulus-le-double-le-ℚ⁺ ε))
+                  ( is-mod-μ ε' (mod-μ ε') (refl-leq-ℕ (mod-μ ε')))))
+```
+
+### Being an accumulation point is equivalent to being a sequential accumulation point
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (X : Located-Metric-Space l1 l2)
+  (S : subset-Located-Metric-Space l3 X)
+  (x : type-Located-Metric-Space X)
+  where
+
+  is-accumulation-point-iff-is-sequential-accumulation-point-subset-Located-Metric-Space :
+    is-accumulation-point-subset-Located-Metric-Space X S x ↔
+    is-sequential-accumulation-point-subset-Located-Metric-Space X S x
+  is-accumulation-point-iff-is-sequential-accumulation-point-subset-Located-Metric-Space =
+    ( is-sequential-accumulation-point-is-accumulation-point-subset-Located-Metric-Space
+        ( X)
+        ( S)
+        ( x) ,
+      is-accumulation-point-is-sequential-accumulation-point-subset-Located-Metric-Space
+        ( X)
+        ( S)
+        ( x))
+```
+
+## External links
+
+- [Accumulation point](https://en.wikipedia.org/wiki/Accumulation_point) on
+  Wikipedia
diff --git a/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md b/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md
index 932310526d..71c916ccf9 100644
--- a/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md
@@ -19,6 +19,7 @@ open import elementary-number-theory.multiplicative-group-of-positive-rational-n
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.nonzero-natural-numbers
 open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
 open import elementary-number-theory.strict-inequality-positive-rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 open import elementary-number-theory.unit-fractions-rational-numbers
@@ -27,6 +28,8 @@ open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositional-truncations
@@ -399,7 +402,7 @@ module _
     map-cauchy-approximation-Metric-Space
       ( M)
       ( x)
-      ( positive-reciprocal-rational-ℕ⁺ (succ-nonzero-ℕ' n))
+      ( positive-reciprocal-rational-succ-ℕ n)
 
   modulus-of-convergence-cauchy-sequence-cauchy-approximation-Metric-Space :
     ℚ⁺ → ℕ
@@ -484,6 +487,49 @@ module _
     is-cauchy-sequence-cauchy-sequence-cauchy-approximation-Metric-Space
 ```
 
+### If a Cauchy approximation has a limit, its corresponding Cauchy sequence has the same limit
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (x : cauchy-approximation-Metric-Space M)
+  (lim : type-Metric-Space M)
+  (is-lim : is-limit-cauchy-approximation-Metric-Space M x lim)
+  where
+
+  abstract
+    is-limit-cauchy-sequence-cauchy-approximation-Metric-Space :
+      is-limit-cauchy-sequence-Metric-Space
+        ( M)
+        ( cauchy-sequence-cauchy-approximation-Metric-Space M x)
+        ( lim)
+    is-limit-cauchy-sequence-cauchy-approximation-Metric-Space =
+      is-limit-bound-modulus-sequence-Metric-Space M _ _
+        ( λ ε →
+          let
+            (n⁺ , 1/n⁺<ε) = smaller-reciprocal-ℚ⁺ ε
+          in
+            ( nat-nonzero-ℕ n⁺ ,
+              λ m n≤m →
+              monotonic-neighborhood-Metric-Space M
+                ( map-cauchy-sequence-cauchy-approximation-Metric-Space M x m)
+                ( lim)
+                ( positive-reciprocal-rational-succ-ℕ m)
+                ( ε)
+                ( transitive-le-ℚ _ (reciprocal-rational-ℕ⁺ n⁺) _
+                  ( 1/n⁺<ε)
+                  ( inv-le-ℚ⁺
+                    ( positive-rational-ℕ⁺ n⁺)
+                    ( positive-rational-ℕ⁺ (succ-nonzero-ℕ' m))
+                    ( preserves-le-rational-ℕ
+                      ( le-succ-leq-ℕ _ _ n≤m))))
+                ( saturated-is-limit-cauchy-approximation-Metric-Space M
+                  ( x)
+                  ( lim)
+                  ( is-lim)
+                  ( positive-reciprocal-rational-succ-ℕ m))))
+```
+
 ### If the Cauchy sequence associated with a Cauchy approximation has a limit modulus at `l`, its associated approximation converges to `l`
 
 ```agda
diff --git a/src/metric-spaces/closed-subsets-located-metric-spaces.lagda.md b/src/metric-spaces/closed-subsets-located-metric-spaces.lagda.md
index 59906ef209..887300e2f4 100644
--- a/src/metric-spaces/closed-subsets-located-metric-spaces.lagda.md
+++ b/src/metric-spaces/closed-subsets-located-metric-spaces.lagda.md
@@ -7,7 +7,9 @@ module metric-spaces.closed-subsets-located-metric-spaces where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
 open import foundation.propositions
+open import foundation.subtypes
 open import foundation.universe-levels
 
 open import metric-spaces.closed-subsets-metric-spaces
@@ -48,4 +50,24 @@ closed-subset-Located-Metric-Space :
   (X : Located-Metric-Space l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l3)
 closed-subset-Located-Metric-Space l3 X =
   closed-subset-Metric-Space l3 (metric-space-Located-Metric-Space X)
+
+subset-closed-subset-Located-Metric-Space :
+  {l1 l2 l3 : Level} (X : Located-Metric-Space l1 l2) →
+  (S : closed-subset-Located-Metric-Space l3 X) →
+  subset-Located-Metric-Space l3 X
+subset-closed-subset-Located-Metric-Space X = pr1
+
+is-closed-subset-closed-subset-Located-Metric-Space :
+  {l1 l2 l3 : Level} (X : Located-Metric-Space l1 l2) →
+  (S : closed-subset-Located-Metric-Space l3 X) →
+  is-closed-subset-Located-Metric-Space
+    ( X)
+    ( subset-closed-subset-Located-Metric-Space X S)
+is-closed-subset-closed-subset-Located-Metric-Space X = pr2
+
+is-in-closed-subset-Located-Metric-Space :
+  {l1 l2 l3 : Level} (X : Located-Metric-Space l1 l2) →
+  (S : closed-subset-Located-Metric-Space l3 X) →
+  type-Located-Metric-Space X → UU l3
+is-in-closed-subset-Located-Metric-Space X S = is-in-subtype (pr1 S)
 ```
diff --git a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md
index 4ba16ab30a..d9a5fe6ea1 100644
--- a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md
+++ b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md
@@ -7,6 +7,7 @@ module metric-spaces.limits-of-cauchy-approximations-metric-spaces where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 
 open import foundation.dependent-pair-types
@@ -20,6 +21,7 @@ open import foundation.universe-levels
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces
 open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
 ```
 
 </details>
@@ -142,6 +144,34 @@ module _
       ( x)
 ```
 
+### The action of short maps on Cauchy approximations preserves limits
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  (f : short-function-Metric-Space A B)
+  (a : cauchy-approximation-Metric-Space A)
+  (lim : type-Metric-Space A)
+  where
+
+  abstract
+    preserves-limit-cauchy-approximation-map-short-function-Metric-Space :
+      is-limit-cauchy-approximation-Metric-Space A a lim →
+      is-limit-cauchy-approximation-Metric-Space
+        ( B)
+        ( map-short-function-cauchy-approximation-Metric-Space A B f a)
+        ( map-short-function-Metric-Space A B f lim)
+    preserves-limit-cauchy-approximation-map-short-function-Metric-Space
+      is-lim-a ε δ =
+      is-short-map-short-function-Metric-Space A B
+        ( f)
+        ( ε +ℚ⁺ δ)
+        ( map-cauchy-approximation-Metric-Space A a ε)
+        ( lim)
+        ( is-lim-a ε δ)
+```
+
 ## See also
 
 - [Convergent cauchy approximations](metric-spaces.convergent-cauchy-approximations-metric-spaces.md)
diff --git a/src/metric-spaces/located-metric-spaces.lagda.md b/src/metric-spaces/located-metric-spaces.lagda.md
index 0da99bc734..5c1f581c70 100644
--- a/src/metric-spaces/located-metric-spaces.lagda.md
+++ b/src/metric-spaces/located-metric-spaces.lagda.md
@@ -133,6 +133,14 @@ module _
   triangular-neighborhood-Located-Metric-Space =
     triangular-neighborhood-Metric-Space metric-space-Located-Metric-Space
 
+  monotonic-neighborhood-Located-Metric-Space :
+    (x y : type-Located-Metric-Space) (d₁ d₂ : ℚ⁺) →
+    le-ℚ⁺ d₁ d₂ →
+    neighborhood-Located-Metric-Space d₁ x y →
+    neighborhood-Located-Metric-Space d₂ x y
+  monotonic-neighborhood-Located-Metric-Space =
+    monotonic-neighborhood-Metric-Space metric-space-Located-Metric-Space
+
   is-located-Located-Metric-Space :
     is-located-Metric-Space metric-space-Located-Metric-Space
   is-located-Located-Metric-Space = pr2 X
@@ -223,3 +231,22 @@ module _
     ( real-dist-located-Metric-Space ,
       is-nonnegative-real-dist-located-Metric-Space)
 ```
+
+### Located metric subspaces
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (X : Located-Metric-Space l1 l2)
+  (S : subset-Located-Metric-Space l3 X)
+  where
+
+  subspace-Located-Metric-Space : Metric-Space (l1 ⊔ l3) l2
+  subspace-Located-Metric-Space =
+    subspace-Metric-Space (metric-space-Located-Metric-Space X) S
+
+  located-subspace-Located-Metric-Space : Located-Metric-Space (l1 ⊔ l3) l2
+  located-subspace-Located-Metric-Space =
+    ( subspace-Located-Metric-Space ,
+      λ (x , _) (y , _) → is-located-Located-Metric-Space X x y)
+```
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index dbf9da826b..139b1a33aa 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -7,6 +7,7 @@ module real-numbers where
 
 open import real-numbers.absolute-value-closed-intervals-real-numbers public
 open import real-numbers.absolute-value-real-numbers public
+open import real-numbers.accumulation-points-subsets-real-numbers public
 open import real-numbers.addition-lower-dedekind-real-numbers public
 open import real-numbers.addition-nonnegative-real-numbers public
 open import real-numbers.addition-real-numbers public
@@ -73,6 +74,7 @@ open import real-numbers.nonzero-real-numbers public
 open import real-numbers.positive-and-negative-real-numbers public
 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-lower-dedekind-real-numbers public
 open import real-numbers.rational-real-numbers public
@@ -84,6 +86,7 @@ open import real-numbers.saturation-inequality-nonnegative-real-numbers public
 open import real-numbers.saturation-inequality-real-numbers public
 open import real-numbers.series-real-numbers public
 open import real-numbers.short-function-binary-maximum-real-numbers public
+open import real-numbers.short-function-binary-minimum-real-numbers public
 open import real-numbers.similarity-nonnegative-real-numbers public
 open import real-numbers.similarity-positive-real-numbers public
 open import real-numbers.similarity-real-numbers public
diff --git a/src/real-numbers/accumulation-points-subsets-real-numbers.lagda.md b/src/real-numbers/accumulation-points-subsets-real-numbers.lagda.md
new file mode 100644
index 0000000000..31cee9ca46
--- /dev/null
+++ b/src/real-numbers/accumulation-points-subsets-real-numbers.lagda.md
@@ -0,0 +1,54 @@
+# Accumulation points of subsets of the real numbers
+
+```agda
+module real-numbers.accumulation-points-subsets-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import lists.sequences
+
+open import metric-spaces.accumulation-points-subsets-located-metric-spaces
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.located-metric-space-of-real-numbers
+open import real-numbers.subsets-real-numbers
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "accumulation point" Disambiguation="of a subset of ℝ" Agda=accumulation-point-subset-ℝ}}
+of a [subset](real-numbers.subsets-real-numbers.md) `S` of the
+[real numbers](real-numbers.dedekind-real-numbers.md) is an
+[accumulation point](metric-spaces.accumulation-points-subsets-located-metric-spaces.md)
+of `S` in the
+[located metric space of the real numbers](real-numbers.located-metric-space-of-real-numbers.md).
+
+### Accumulation points of subsets of ℝ
+
+```agda
+module _
+  {l1 l2 : Level} (S : subset-ℝ l1 l2)
+  where
+
+  is-accumulation-point-prop-subset-ℝ : subset-ℝ (l1 ⊔ lsuc l2) l2
+  is-accumulation-point-prop-subset-ℝ =
+    is-accumulation-point-prop-subset-Located-Metric-Space
+      ( located-metric-space-ℝ l2)
+      ( S)
+
+  is-accumulation-point-subset-ℝ : ℝ l2 → UU (l1 ⊔ lsuc l2)
+  is-accumulation-point-subset-ℝ x =
+    type-Prop (is-accumulation-point-prop-subset-ℝ x)
+
+  accumulation-point-subset-ℝ : UU (l1 ⊔ lsuc l2)
+  accumulation-point-subset-ℝ = type-subtype is-accumulation-point-prop-subset-ℝ
+```
diff --git a/src/real-numbers/apartness-real-numbers.lagda.md b/src/real-numbers/apartness-real-numbers.lagda.md
index 47a55ed6a5..5529df3497 100644
--- a/src/real-numbers/apartness-real-numbers.lagda.md
+++ b/src/real-numbers/apartness-real-numbers.lagda.md
@@ -67,6 +67,10 @@ module _
 apart-le-ℝ :
   {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → le-ℝ x y → apart-ℝ x y
 apart-le-ℝ = inl-disjunction
+
+apart-le-ℝ' :
+  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → le-ℝ y x → apart-ℝ x y
+apart-le-ℝ' = inr-disjunction
 ```
 
 ## Properties
diff --git a/src/real-numbers/binary-maximum-real-numbers.lagda.md b/src/real-numbers/binary-maximum-real-numbers.lagda.md
index d4da7d69c0..b225ca7890 100644
--- a/src/real-numbers/binary-maximum-real-numbers.lagda.md
+++ b/src/real-numbers/binary-maximum-real-numbers.lagda.md
@@ -9,8 +9,11 @@ module real-numbers.binary-maximum-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 
+open import foundation.action-on-identifications-binary-functions
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.empty-types
@@ -106,6 +109,11 @@ module _
         ( upper-real-max-ℝ)
         ( is-disjoint-lower-upper-max-ℝ)
         ( is-located-lower-upper-max-ℝ)
+
+ap-max-ℝ :
+  {l1 l2 : Level} → {x x' : ℝ l1} → x ＝ x' →
+  {y y' : ℝ l2} → y ＝ y' → max-ℝ x y ＝ max-ℝ x' y'
+ap-max-ℝ = ap-binary max-ℝ
 ```
 
 ## Properties
@@ -375,3 +383,53 @@ module _
               ( is-located-lower-upper-cut-ℝ y q<r))
           ( is-located-lower-upper-cut-ℝ x q<r)
 ```
+
+### If `x < z` and `y < z`, then `max-ℝ x y < z`
+
+```agda
+abstract
+  le-max-le-le-ℝ :
+    {l1 l2 l3 : Level} {x : ℝ l1} {y : ℝ l2} {z : ℝ l3} → le-ℝ x z → le-ℝ y z →
+    le-ℝ (max-ℝ x y) z
+  le-max-le-le-ℝ {x = x} {y = y} {z = z} x<z y<z =
+    let open do-syntax-trunc-Prop (le-prop-ℝ (max-ℝ x y) z)
+    in do
+      (p , x<p , p<z) ← dense-rational-le-ℝ x z x<z
+      (q , y<q , q<z) ← dense-rational-le-ℝ y z y<z
+      rec-coproduct
+        ( λ p≤q →
+          concatenate-leq-le-ℝ
+            ( max-ℝ x y)
+            ( real-ℚ q)
+            ( z)
+            ( leq-max-leq-leq-ℝ
+              ( x)
+              ( y)
+              ( real-ℚ q)
+              ( transitive-leq-ℝ
+                ( x)
+                ( real-ℚ p)
+                ( real-ℚ q)
+                ( preserves-leq-real-ℚ p≤q)
+                ( leq-le-ℝ x<p))
+              ( leq-le-ℝ y<q))
+            ( q<z))
+        ( λ q≤p →
+          concatenate-leq-le-ℝ
+            ( max-ℝ x y)
+            ( real-ℚ p)
+            ( z)
+            ( leq-max-leq-leq-ℝ
+              ( x)
+              ( y)
+              ( real-ℚ p)
+              ( leq-le-ℝ x<p)
+              ( transitive-leq-ℝ
+                ( y)
+                ( real-ℚ q)
+                ( real-ℚ p)
+                ( preserves-leq-real-ℚ q≤p)
+                ( leq-le-ℝ y<q)))
+            ( p<z))
+        ( linear-leq-ℚ p q)
+```
diff --git a/src/real-numbers/binary-minimum-real-numbers.lagda.md b/src/real-numbers/binary-minimum-real-numbers.lagda.md
index b0ae4c0640..37f19c055e 100644
--- a/src/real-numbers/binary-minimum-real-numbers.lagda.md
+++ b/src/real-numbers/binary-minimum-real-numbers.lagda.md
@@ -11,6 +11,8 @@ module real-numbers.binary-minimum-real-numbers where
 ```agda
 open import elementary-number-theory.positive-rational-numbers
 
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.dependent-pair-types
 open import foundation.disjunction
@@ -30,6 +32,7 @@ open import real-numbers.difference-real-numbers
 open import real-numbers.inequality-real-numbers
 open import real-numbers.negation-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 ```
 
@@ -54,6 +57,11 @@ module _
   opaque
     min-ℝ : ℝ (l1 ⊔ l2)
     min-ℝ = neg-ℝ (max-ℝ (neg-ℝ x) (neg-ℝ y))
+
+ap-min-ℝ :
+  {l1 l2 : Level} → {x x' : ℝ l1} → x ＝ x' →
+  {y y' : ℝ l2} → y ＝ y' → min-ℝ x y ＝ min-ℝ x' y'
+ap-min-ℝ = ap-binary min-ℝ
 ```
 
 ## Properties
@@ -130,6 +138,18 @@ module _
           ( is-greatest-binary-lower-bound-min-ℝ x y))
 ```
 
+### The binary minimum is commutative
+
+```agda
+abstract opaque
+  unfolding min-ℝ
+
+  commutative-min-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → min-ℝ x y ＝ min-ℝ y x
+  commutative-min-ℝ x y =
+    ap neg-ℝ (commutative-max-ℝ (neg-ℝ x) (neg-ℝ y))
+```
+
 ### The large poset of real numbers has meets
 
 ```agda
@@ -183,3 +203,43 @@ module _
           ( λ max-ε<-y → inr-disjunction (case y max-ε<-y))
           ( approximate-below-max-ℝ (neg-ℝ x) (neg-ℝ y) ε)
 ```
+
+### If `x ≤ y`, the minimum of `x` and `y` is similar to `x`
+
+```agda
+abstract opaque
+  unfolding min-ℝ
+
+  left-leq-right-min-ℝ :
+    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → leq-ℝ x y →
+    sim-ℝ (min-ℝ x y) x
+  left-leq-right-min-ℝ {x = x} {y = y} x≤y =
+    similarity-reasoning-ℝ
+      min-ℝ x y
+      ~ℝ neg-ℝ (neg-ℝ x)
+        by preserves-sim-neg-ℝ (right-leq-left-max-ℝ (neg-leq-ℝ x≤y))
+      ~ℝ x
+        by sim-eq-ℝ (neg-neg-ℝ x)
+
+  right-leq-left-min-ℝ :
+    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → leq-ℝ y x →
+    sim-ℝ (min-ℝ x y) y
+  right-leq-left-min-ℝ {y = y} y≤x =
+    tr (λ z → sim-ℝ z y) (commutative-min-ℝ _ _) (left-leq-right-min-ℝ y≤x)
+```
+
+### If `x < y` and `x < z`, then `x < min-ℝ y z`
+
+```agda
+abstract opaque
+  unfolding min-ℝ
+
+  le-min-le-le-ℝ :
+    {l1 l2 l3 : Level} {x : ℝ l1} {y : ℝ l2} {z : ℝ l3} → le-ℝ x y → le-ℝ x z →
+    le-ℝ x (min-ℝ y z)
+  le-min-le-le-ℝ {x = x} {y = y} {z = z} x<y x<z =
+    tr
+      ( λ w → le-ℝ w (min-ℝ y z))
+      ( neg-neg-ℝ x)
+      ( neg-le-ℝ (le-max-le-le-ℝ (neg-le-ℝ x<y) (neg-le-ℝ x<z)))
+```
diff --git a/src/real-numbers/closed-intervals-real-numbers.lagda.md b/src/real-numbers/closed-intervals-real-numbers.lagda.md
index 09d4fada9e..dab0a49654 100644
--- a/src/real-numbers/closed-intervals-real-numbers.lagda.md
+++ b/src/real-numbers/closed-intervals-real-numbers.lagda.md
@@ -23,14 +23,20 @@ open import foundation.universe-levels
 open import metric-spaces.closed-subsets-metric-spaces
 open import metric-spaces.complete-metric-spaces
 open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.subspaces-metric-spaces
 
 open import order-theory.closed-intervals-large-posets
 
+open import real-numbers.binary-maximum-real-numbers
+open import real-numbers.binary-minimum-real-numbers
 open import real-numbers.cauchy-completeness-dedekind-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.inequality-real-numbers
 open import real-numbers.metric-space-of-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.short-function-binary-maximum-real-numbers
+open import real-numbers.short-function-binary-minimum-real-numbers
 ```
 
 </details>
@@ -64,6 +70,11 @@ subtype-closed-interval-ℝ :
   subtype (l1 ⊔ l2 ⊔ l) (ℝ l)
 subtype-closed-interval-ℝ = subtype-closed-interval-Large-Poset ℝ-Large-Poset
 
+type-closed-interval-ℝ :
+  {l1 l2 : Level} (l : Level) → closed-interval-ℝ l1 l2 → UU (l1 ⊔ l2 ⊔ lsuc l)
+type-closed-interval-ℝ l [a,b] =
+  type-subtype (subtype-closed-interval-ℝ l [a,b])
+
 lower-bound-closed-interval-ℝ : {l1 l2 : Level} → closed-interval-ℝ l1 l2 → ℝ l1
 lower-bound-closed-interval-ℝ =
   lower-bound-closed-interval-Large-Poset ℝ-Large-Poset
@@ -161,3 +172,44 @@ complete-metric-space-unit-interval-ℝ :
 complete-metric-space-unit-interval-ℝ l =
   complete-metric-space-closed-interval-ℝ l unit-closed-interval-ℝ
 ```
+
+### The clamping function
+
+```agda
+clamp-closed-interval-ℝ :
+  {l1 l2 l3 : Level} ([a,b] : closed-interval-ℝ l1 l2) → ℝ l3 →
+  type-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b]
+clamp-closed-interval-ℝ ((a , b) , a≤b) x =
+  ( max-ℝ a (min-ℝ b x) ,
+    leq-left-max-ℝ _ _ ,
+    leq-max-leq-leq-ℝ _ _ _ a≤b (leq-left-min-ℝ b x))
+```
+
+### The clamping function is a short function
+
+```agda
+abstract
+  is-short-clamp-closed-interval-ℝ :
+    {l1 l2 l3 : Level} ([a,b] : closed-interval-ℝ l1 l2) →
+    is-short-function-Metric-Space
+      ( metric-space-ℝ l3)
+      ( metric-space-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b])
+      ( clamp-closed-interval-ℝ [a,b])
+  is-short-clamp-closed-interval-ℝ [a,b]@((a , b) , a≤b) =
+    is-short-comp-is-short-function-Metric-Space
+      ( metric-space-ℝ _)
+      ( metric-space-ℝ _)
+      ( metric-space-ℝ _)
+      ( max-ℝ a)
+      ( min-ℝ b)
+      ( is-short-function-left-max-ℝ a)
+      ( is-short-function-left-min-ℝ b)
+
+short-clamp-closed-interval-ℝ :
+  {l1 l2 l3 : Level} ([a,b] : closed-interval-ℝ l1 l2) →
+  short-function-Metric-Space
+    ( metric-space-ℝ l3)
+    ( metric-space-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b])
+short-clamp-closed-interval-ℝ [a,b] =
+  ( clamp-closed-interval-ℝ [a,b] , is-short-clamp-closed-interval-ℝ [a,b])
+```
diff --git a/src/real-numbers/isometry-addition-real-numbers.lagda.md b/src/real-numbers/isometry-addition-real-numbers.lagda.md
index 3b1ca98943..15906cfdbd 100644
--- a/src/real-numbers/isometry-addition-real-numbers.lagda.md
+++ b/src/real-numbers/isometry-addition-real-numbers.lagda.md
@@ -18,6 +18,8 @@ open import metric-spaces.cartesian-products-metric-spaces
 open import metric-spaces.isometries-metric-spaces
 open import metric-spaces.metric-space-of-isometries-metric-spaces
 open import metric-spaces.modulated-uniformly-continuous-functions-metric-spaces
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
 
 open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
@@ -94,6 +96,16 @@ module _
       ( metric-space-ℝ l2)
       ( metric-space-ℝ (l1 ⊔ l2))
   isometry-right-add-ℝ = ( (λ y → add-ℝ y x) , is-isometry-right-add-ℝ)
+
+  short-left-add-ℝ :
+    short-function-Metric-Space
+      ( metric-space-ℝ l2)
+      ( metric-space-ℝ (l1 ⊔ l2))
+  short-left-add-ℝ =
+    short-isometry-Metric-Space
+      ( metric-space-ℝ l2)
+      ( metric-space-ℝ (l1 ⊔ l2))
+      ( isometry-left-add-ℝ)
 ```
 
 ### Addition is an isometry from `ℝ` to the metric space of isometries `ℝ → ℝ`
diff --git a/src/real-numbers/isometry-difference-real-numbers.lagda.md b/src/real-numbers/isometry-difference-real-numbers.lagda.md
index 73b411df6a..6b909afc88 100644
--- a/src/real-numbers/isometry-difference-real-numbers.lagda.md
+++ b/src/real-numbers/isometry-difference-real-numbers.lagda.md
@@ -13,6 +13,7 @@ open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
 open import metric-spaces.isometries-metric-spaces
+open import metric-spaces.short-functions-metric-spaces
 open import metric-spaces.uniformly-continuous-functions-metric-spaces
 
 open import real-numbers.addition-real-numbers
@@ -61,6 +62,14 @@ module _
     isometry-Metric-Space (metric-space-ℝ l2) (metric-space-ℝ (l1 ⊔ l2))
   isometry-diff-ℝ = (diff-ℝ x , is-isometry-diff-ℝ)
 
+  short-diff-ℝ :
+    short-function-Metric-Space (metric-space-ℝ l2) (metric-space-ℝ (l1 ⊔ l2))
+  short-diff-ℝ =
+    short-isometry-Metric-Space
+      ( metric-space-ℝ l2)
+      ( metric-space-ℝ (l1 ⊔ l2))
+      ( isometry-diff-ℝ)
+
   uniformly-continuous-diff-ℝ :
     uniformly-continuous-function-Metric-Space
       ( metric-space-ℝ l2)
diff --git a/src/real-numbers/isometry-negation-real-numbers.lagda.md b/src/real-numbers/isometry-negation-real-numbers.lagda.md
index 3c2b449432..05c832b67f 100644
--- a/src/real-numbers/isometry-negation-real-numbers.lagda.md
+++ b/src/real-numbers/isometry-negation-real-numbers.lagda.md
@@ -20,6 +20,8 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import metric-spaces.isometries-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
 
 open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
@@ -122,3 +124,21 @@ module _
       ( metric-space-ℝ l1)
   isometry-neg-ℝ = (neg-ℝ , is-isometry-neg-ℝ)
 ```
+
+### Negation on the real numbers is short
+
+```agda
+abstract
+  is-short-neg-ℝ :
+    {l : Level} →
+    is-short-function-Metric-Space
+      ( metric-space-ℝ l)
+      ( metric-space-ℝ l)
+      ( neg-ℝ)
+  is-short-neg-ℝ =
+    is-short-is-isometry-Metric-Space
+      ( metric-space-ℝ _)
+      ( metric-space-ℝ _)
+      ( neg-ℝ)
+      ( is-isometry-neg-ℝ)
+```
diff --git a/src/real-numbers/proper-closed-intervals-real-numbers.lagda.md b/src/real-numbers/proper-closed-intervals-real-numbers.lagda.md
new file mode 100644
index 0000000000..fa15226a2a
--- /dev/null
+++ b/src/real-numbers/proper-closed-intervals-real-numbers.lagda.md
@@ -0,0 +1,376 @@
+# Proper closed intervals in the real numbers
+
+```agda
+module real-numbers.proper-closed-intervals-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.unit-fractions-rational-numbers
+
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.closed-subsets-metric-spaces
+open import metric-spaces.complete-metric-spaces
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
+open import metric-spaces.metric-space-of-rational-numbers
+open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.subspaces-metric-spaces
+
+open import order-theory.large-posets
+
+open import real-numbers.accumulation-points-subsets-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.apartness-real-numbers
+open import real-numbers.binary-maximum-real-numbers
+open import real-numbers.binary-minimum-real-numbers
+open import real-numbers.closed-intervals-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.isometry-addition-real-numbers
+open import real-numbers.isometry-difference-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+open import real-numbers.subsets-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "proper closed interval" Disambiguation="in ℝ" Agda=proper-closed-interval-ℝ}}
+in the [real numbers](real-numbers.dedekind-real-numbers.md) is a
+[closed interval](real-numbers.closed-intervals-real-numbers.md) in which the
+lower bound is
+[strictly less than](real-numbers.strict-inequality-real-numbers.md) the upper
+bound.
+
+## Definition
+
+```agda
+proper-closed-interval-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+proper-closed-interval-ℝ l1 l2 = Σ (ℝ l1) (λ x → Σ (ℝ l2) (λ y → le-ℝ x y))
+
+closed-interval-proper-closed-interval-ℝ :
+  {l1 l2 : Level} → proper-closed-interval-ℝ l1 l2 → closed-interval-ℝ l1 l2
+closed-interval-proper-closed-interval-ℝ (a , b , a<b) =
+  ((a , b) , leq-le-ℝ a<b)
+
+lower-bound-proper-closed-interval-ℝ :
+  {l1 l2 : Level} → proper-closed-interval-ℝ l1 l2 → ℝ l1
+lower-bound-proper-closed-interval-ℝ (a , b , a<b) = a
+
+upper-bound-proper-closed-interval-ℝ :
+  {l1 l2 : Level} → proper-closed-interval-ℝ l1 l2 → ℝ l2
+upper-bound-proper-closed-interval-ℝ (a , b , a<b) = b
+
+subtype-proper-closed-interval-ℝ :
+  {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 →
+  subset-ℝ (l1 ⊔ l2 ⊔ l) l
+subtype-proper-closed-interval-ℝ l (a , b , _) x =
+  leq-prop-ℝ a x ∧ leq-prop-ℝ x b
+
+is-in-proper-closed-interval-ℝ :
+  {l1 l2 l3 : Level} → proper-closed-interval-ℝ l1 l2 → ℝ l3 → UU (l1 ⊔ l2 ⊔ l3)
+is-in-proper-closed-interval-ℝ (a , b , _) x = leq-ℝ a x × leq-ℝ x b
+
+type-proper-closed-interval-ℝ :
+  {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 →
+  UU (l1 ⊔ l2 ⊔ lsuc l)
+type-proper-closed-interval-ℝ l [a,b] =
+  type-subtype (subtype-proper-closed-interval-ℝ l [a,b])
+```
+
+## Properties
+
+### The metric space associated with a proper closed interval
+
+```agda
+metric-space-proper-closed-interval-ℝ :
+  {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 →
+  Metric-Space (l1 ⊔ l2 ⊔ lsuc l) l
+metric-space-proper-closed-interval-ℝ l [a,b] =
+  metric-space-closed-interval-ℝ
+    ( l)
+    ( closed-interval-proper-closed-interval-ℝ [a,b])
+```
+
+### The metric space associated with a proper closed interval is closed
+
+```agda
+abstract
+  is-closed-subset-proper-closed-interval-ℝ :
+    {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) →
+    is-closed-subset-Metric-Space
+      ( metric-space-ℝ l3)
+      ( subtype-proper-closed-interval-ℝ l3 [a,b])
+  is-closed-subset-proper-closed-interval-ℝ [a,b] =
+    is-closed-subset-closed-interval-ℝ
+      ( closed-interval-proper-closed-interval-ℝ [a,b])
+
+closed-subset-proper-closed-interval-ℝ :
+  {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 →
+  closed-subset-Metric-Space (l1 ⊔ l2 ⊔ l) (metric-space-ℝ l)
+closed-subset-proper-closed-interval-ℝ l [a,b] =
+  closed-subset-closed-interval-ℝ
+    ( l)
+    ( closed-interval-proper-closed-interval-ℝ [a,b])
+```
+
+### The complete metric space associated with a proper closed interval
+
+```agda
+complete-metric-space-proper-closed-interval-ℝ :
+  {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 →
+  Complete-Metric-Space (l1 ⊔ l2 ⊔ lsuc l) l
+complete-metric-space-proper-closed-interval-ℝ l [a,b] =
+  complete-metric-space-closed-interval-ℝ
+    ( l)
+    ( closed-interval-proper-closed-interval-ℝ [a,b])
+```
+
+### The clamp function
+
+```agda
+clamp-proper-closed-interval-ℝ :
+  {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) → ℝ l3 →
+  type-proper-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b]
+clamp-proper-closed-interval-ℝ [a,b] =
+  clamp-closed-interval-ℝ (closed-interval-proper-closed-interval-ℝ [a,b])
+```
+
+### The clamp function is a short function
+
+```agda
+abstract
+  is-short-clamp-proper-closed-interval-ℝ :
+    {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) →
+    is-short-function-Metric-Space
+      ( metric-space-ℝ l3)
+      ( metric-space-proper-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b])
+      ( clamp-proper-closed-interval-ℝ [a,b])
+  is-short-clamp-proper-closed-interval-ℝ [a,b] =
+    is-short-clamp-closed-interval-ℝ
+      ( closed-interval-proper-closed-interval-ℝ [a,b])
+
+short-clamp-proper-closed-interval-ℝ :
+  {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) →
+  short-function-Metric-Space
+    ( metric-space-ℝ l3)
+    ( metric-space-proper-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b])
+short-clamp-proper-closed-interval-ℝ [a,b] =
+  short-clamp-closed-interval-ℝ (closed-interval-proper-closed-interval-ℝ [a,b])
+```
+
+### Every real number in a proper closed interval is an accumulation point in that proper closed interval
+
+Note that this cannot be made more universe-polymorphic.
+
+```agda
+abstract
+  is-accumulation-point-le-upper-bound-proper-closed-interval-ℝ :
+    {l : Level} ([a,b] : proper-closed-interval-ℝ l l) →
+    (x : ℝ l) → is-in-proper-closed-interval-ℝ [a,b] x →
+    le-ℝ x (upper-bound-proper-closed-interval-ℝ [a,b]) →
+    is-accumulation-point-subset-ℝ
+      ( subtype-proper-closed-interval-ℝ l [a,b])
+      ( x)
+  is-accumulation-point-le-upper-bound-proper-closed-interval-ℝ
+    {l} [a,b]@(a , b , a<b) x (a≤x , x≤b) x<b =
+    let
+      open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      motive =
+        is-accumulation-point-prop-subset-ℝ
+          ( subtype-proper-closed-interval-ℝ _ [a,b])
+          ( x)
+      short-clamp-add =
+        comp-short-function-Metric-Space
+          ( metric-space-ℚ)
+          ( metric-space-ℝ lzero)
+          ( metric-space-proper-closed-interval-ℝ l [a,b])
+          ( comp-short-function-Metric-Space
+            ( metric-space-ℝ lzero)
+            ( metric-space-ℝ l)
+            ( metric-space-proper-closed-interval-ℝ l [a,b])
+            ( short-clamp-proper-closed-interval-ℝ [a,b])
+            ( short-left-add-ℝ x))
+          ( short-isometry-Metric-Space
+            ( metric-space-ℚ)
+            ( metric-space-ℝ lzero)
+            ( isometry-metric-space-real-ℚ))
+      short-inclusion =
+        short-inclusion-subspace-Metric-Space
+          ( metric-space-ℝ l)
+          ( subtype-proper-closed-interval-ℝ l [a,b])
+      approx-clamp-add =
+        map-short-function-cauchy-approximation-Metric-Space
+          ( metric-space-ℚ)
+          ( metric-space-proper-closed-interval-ℝ l [a,b])
+          ( short-clamp-add)
+          ( cauchy-approximation-rational-ℚ⁺)
+    in
+      intro-exists
+        ( approx-clamp-add)
+        ( ( λ ε →
+            apart-located-metric-space-apart-ℝ _ _
+              ( apart-le-ℝ'
+                ( concatenate-le-leq-ℝ
+                  ( x)
+                  ( min-ℝ b (x +ℝ real-ℚ⁺ ε))
+                  ( max-ℝ a (min-ℝ b (x +ℝ real-ℚ⁺ ε)))
+                  ( le-min-le-le-ℝ
+                    ( x<b)
+                    ( le-left-add-real-ℝ⁺ x (positive-real-ℚ⁺ ε)))
+                  ( leq-right-max-ℝ _ _)))) ,
+          tr
+            ( is-limit-cauchy-approximation-Metric-Space
+              ( metric-space-ℝ l)
+              ( map-short-function-cauchy-approximation-Metric-Space
+                ( metric-space-proper-closed-interval-ℝ l [a,b])
+                ( metric-space-ℝ l)
+                ( short-inclusion)
+                ( approx-clamp-add)))
+            ( equational-reasoning
+              max-ℝ a (min-ℝ b (x +ℝ zero-ℝ))
+              ＝ max-ℝ a (min-ℝ b x)
+                by ap-max-ℝ refl (ap-min-ℝ refl (right-unit-law-add-ℝ x))
+              ＝ max-ℝ a x
+                by ap-max-ℝ refl (eq-sim-ℝ (right-leq-left-min-ℝ x≤b))
+              ＝ x
+                by eq-sim-ℝ (left-leq-right-max-ℝ a≤x))
+            ( preserves-limit-cauchy-approximation-map-short-function-Metric-Space
+              ( metric-space-ℚ)
+              ( metric-space-ℝ l)
+              ( comp-short-function-Metric-Space
+                ( metric-space-ℚ)
+                ( metric-space-proper-closed-interval-ℝ l [a,b])
+                ( metric-space-ℝ l)
+                ( short-inclusion)
+                ( short-clamp-add))
+              ( cauchy-approximation-rational-ℚ⁺)
+              ( zero-ℚ)
+              ( is-zero-limit-rational-ℚ⁺)))
+
+  is-accumulation-point-le-lower-bound-proper-closed-interval-ℝ :
+    {l : Level} ([a,b] : proper-closed-interval-ℝ l l) →
+    (x : ℝ l) → is-in-proper-closed-interval-ℝ [a,b] x →
+    le-ℝ (lower-bound-proper-closed-interval-ℝ [a,b]) x →
+    is-accumulation-point-subset-ℝ
+      ( subtype-proper-closed-interval-ℝ l [a,b])
+      ( x)
+  is-accumulation-point-le-lower-bound-proper-closed-interval-ℝ
+    {l} [a,b]@(a , b , a<b) x (a≤x , x≤b) a<x =
+    let
+      open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      motive =
+        is-accumulation-point-prop-subset-ℝ
+          ( subtype-proper-closed-interval-ℝ _ [a,b])
+          ( x)
+      short-clamp-diff =
+        comp-short-function-Metric-Space
+          ( metric-space-ℚ)
+          ( metric-space-ℝ lzero)
+          ( metric-space-proper-closed-interval-ℝ l [a,b])
+          ( comp-short-function-Metric-Space
+            ( metric-space-ℝ lzero)
+            ( metric-space-ℝ l)
+            ( metric-space-proper-closed-interval-ℝ l [a,b])
+            ( short-clamp-proper-closed-interval-ℝ [a,b])
+            ( short-diff-ℝ x))
+          ( short-isometry-Metric-Space
+            ( metric-space-ℚ)
+            ( metric-space-ℝ lzero)
+            ( isometry-metric-space-real-ℚ))
+      short-inclusion =
+        short-inclusion-subspace-Metric-Space
+          ( metric-space-ℝ l)
+          ( subtype-proper-closed-interval-ℝ l [a,b])
+      approx-clamp-diff =
+        map-short-function-cauchy-approximation-Metric-Space
+          ( metric-space-ℚ)
+          ( metric-space-proper-closed-interval-ℝ l [a,b])
+          ( short-clamp-diff)
+          ( cauchy-approximation-rational-ℚ⁺)
+    in
+      intro-exists
+        ( approx-clamp-diff)
+        ( ( λ ε →
+            apart-located-metric-space-apart-ℝ _ _
+              ( apart-le-ℝ
+                ( le-max-le-le-ℝ
+                  ( a<x)
+                  ( concatenate-leq-le-ℝ
+                    ( min-ℝ b (x -ℝ real-ℚ⁺ ε))
+                    ( x -ℝ real-ℚ⁺ ε)
+                    ( x)
+                    ( leq-right-min-ℝ _ _)
+                    ( le-diff-real-ℝ⁺ x (positive-real-ℚ⁺ ε)))))) ,
+          tr
+            ( is-limit-cauchy-approximation-Metric-Space
+              ( metric-space-ℝ l)
+              ( map-short-function-cauchy-approximation-Metric-Space
+                ( metric-space-proper-closed-interval-ℝ l [a,b])
+                ( metric-space-ℝ l)
+                ( short-inclusion)
+                ( approx-clamp-diff)))
+            ( equational-reasoning
+              max-ℝ a (min-ℝ b (x -ℝ zero-ℝ))
+              ＝ max-ℝ a (min-ℝ b x)
+                by ap-max-ℝ refl (ap-min-ℝ refl (right-unit-law-diff-ℝ x))
+              ＝ max-ℝ a x
+                by
+                  ap-max-ℝ refl (eq-sim-ℝ (right-leq-left-min-ℝ x≤b))
+              ＝ x
+                by eq-sim-ℝ (left-leq-right-max-ℝ a≤x))
+            ( preserves-limit-cauchy-approximation-map-short-function-Metric-Space
+              ( metric-space-ℚ)
+              ( metric-space-ℝ l)
+              ( comp-short-function-Metric-Space
+                ( metric-space-ℚ)
+                ( metric-space-proper-closed-interval-ℝ l [a,b])
+                ( metric-space-ℝ l)
+                ( short-inclusion)
+                ( short-clamp-diff))
+              ( cauchy-approximation-rational-ℚ⁺)
+              ( zero-ℚ)
+              ( is-zero-limit-rational-ℚ⁺)))
+
+  is-accumulation-point-is-in-proper-closed-interval-ℝ :
+    {l : Level} ([a,b] : proper-closed-interval-ℝ l l) →
+    (x : ℝ l) → is-in-proper-closed-interval-ℝ [a,b] x →
+    is-accumulation-point-subset-ℝ
+      ( subtype-proper-closed-interval-ℝ l [a,b])
+      ( x)
+  is-accumulation-point-is-in-proper-closed-interval-ℝ
+    {l} [a,b]@(a , b , a<b) x a≤x≤b =
+    elim-disjunction
+      ( is-accumulation-point-prop-subset-ℝ
+        ( subtype-proper-closed-interval-ℝ _ [a,b])
+        ( x))
+      ( is-accumulation-point-le-lower-bound-proper-closed-interval-ℝ
+        ( [a,b])
+        ( x)
+        ( a≤x≤b))
+      ( is-accumulation-point-le-upper-bound-proper-closed-interval-ℝ
+        ( [a,b])
+        ( x)
+        ( a≤x≤b))
+      ( cotransitive-le-ℝ a b x a<b)
+```
diff --git a/src/real-numbers/short-function-binary-maximum-real-numbers.lagda.md b/src/real-numbers/short-function-binary-maximum-real-numbers.lagda.md
index 9cca40873e..d0716d0b19 100644
--- a/src/real-numbers/short-function-binary-maximum-real-numbers.lagda.md
+++ b/src/real-numbers/short-function-binary-maximum-real-numbers.lagda.md
@@ -17,6 +17,7 @@ open import foundation.universe-levels
 
 open import metric-spaces.metric-space-of-short-functions-metric-spaces
 open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
 
 open import order-theory.least-upper-bounds-large-posets
 
@@ -29,6 +30,7 @@ open import real-numbers.metric-space-of-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.strict-inequality-real-numbers
+open import real-numbers.uniformly-continuous-functions-real-numbers
 ```
 
 </details>
@@ -128,6 +130,13 @@ module _
       ( metric-space-ℝ (l1 ⊔ l2))
   short-left-max-ℝ =
     (max-ℝ x , is-short-function-left-max-ℝ)
+
+  uniformly-continuous-left-max-ℝ : uniformly-continuous-function-ℝ l2 (l1 ⊔ l2)
+  uniformly-continuous-left-max-ℝ =
+    uniformly-continuous-short-function-Metric-Space
+      ( metric-space-ℝ l2)
+      ( metric-space-ℝ (l1 ⊔ l2))
+      ( short-left-max-ℝ)
 ```
 
 ### The binary maximum is a short function from `ℝ` to the metric space of short functions `ℝ → ℝ`
diff --git a/src/real-numbers/short-function-binary-minimum-real-numbers.lagda.md b/src/real-numbers/short-function-binary-minimum-real-numbers.lagda.md
new file mode 100644
index 0000000000..5ad2465841
--- /dev/null
+++ b/src/real-numbers/short-function-binary-minimum-real-numbers.lagda.md
@@ -0,0 +1,72 @@
+# The binary minimum of real numbers is a short function
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.short-function-binary-minimum-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.short-functions-metric-spaces
+
+open import real-numbers.binary-maximum-real-numbers
+open import real-numbers.binary-minimum-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.isometry-negation-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.short-function-binary-maximum-real-numbers
+```
+
+</details>
+
+## Idea
+
+For any `a : ℝ`, the
+[binary minimum](real-numbers.binary-minimum-real-numbers.md) with `a` is a
+[short function](metric-spaces.short-functions-metric-spaces.md) `ℝ → ℝ` for the
+[standard real metric structure](real-numbers.metric-space-of-real-numbers.md).
+
+## Proof
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1)
+  where
+
+  abstract opaque
+    unfolding min-ℝ
+
+    is-short-function-left-min-ℝ :
+      is-short-function-Metric-Space
+        ( metric-space-ℝ l2)
+        ( metric-space-ℝ (l1 ⊔ l2))
+        ( min-ℝ x)
+    is-short-function-left-min-ℝ =
+      is-short-comp-is-short-function-Metric-Space
+        ( metric-space-ℝ l2)
+        ( metric-space-ℝ (l1 ⊔ l2))
+        ( metric-space-ℝ (l1 ⊔ l2))
+        ( neg-ℝ)
+        ( λ y → max-ℝ (neg-ℝ x) (neg-ℝ y))
+        ( is-short-neg-ℝ)
+        ( is-short-comp-is-short-function-Metric-Space
+          ( metric-space-ℝ l2)
+          ( metric-space-ℝ l2)
+          ( metric-space-ℝ (l1 ⊔ l2))
+          ( max-ℝ (neg-ℝ x))
+          ( neg-ℝ)
+          ( is-short-function-left-max-ℝ (neg-ℝ x))
+          ( is-short-neg-ℝ))
+
+  short-left-min-ℝ :
+    short-function-Metric-Space
+      ( metric-space-ℝ l2)
+      ( metric-space-ℝ (l1 ⊔ l2))
+  short-left-min-ℝ = (min-ℝ x , is-short-function-left-min-ℝ)
+```