make pre-commit

UniMath · Feb 15, 2025 · 507492a · 507492a
1 parent 1d6c62a
commit 507492a
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md
@@ -49,8 +49,8 @@ is
 if for any [positive](elementary-number-theory.positive-rational-numbers.md)
 [rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ⁺`, there
 exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that `0 < q - p < ε`.
-Intuitively, when `L` and `U` are the lower and upper cuts of a real number `x`, then `p` and `q`
-are rational approximations of `x` to within `ε`.
+Intuitively, when `L` and `U` are the lower and upper cuts of a real number `x`,
+then `p` and `q` are rational approximations of `x` to within `ε`.
 
 This follows parts of Section 11 in {{#cite BauerTaylor2009}}.
 

diff --git a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md
@@ -40,10 +40,11 @@ open import real-numbers.upper-dedekind-real-numbers
 
 ## Idea
 
-The {{#concept "negation" Disambiguation="of a one-sided Dedekind real number" Agda=neg-lower-ℝ Agda=neg-upper-ℝ}} of a
-[lower Dedekind real number](real-numbers.lower-dedekind-real-numbers.md) is an
-[upper Dedekind real number](real-numbers.upper-dedekind-real-numbers.md) whose
-cut contains negations of elements in the lower cut, and vice versa.
+The
+{{#concept "negation" Disambiguation="of a one-sided Dedekind real number" Agda=neg-lower-ℝ Agda=neg-upper-ℝ}}
+of a [lower Dedekind real number](real-numbers.lower-dedekind-real-numbers.md)
+is an [upper Dedekind real number](real-numbers.upper-dedekind-real-numbers.md)
+whose cut contains negations of elements in the lower cut, and vice versa.
 
 ## Definitions