From 380382bfd9c357f6017d92126b8533f7b2065606 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 7 Nov 2025 14:41:01 -0800 Subject: [PATCH 01/21] Progress --- .../absolute-value-rational-numbers.lagda.md | 2 +- ...ddition-positive-rational-numbers.lagda.md | 13 +- .../distance-rational-numbers.lagda.md | 5 +- .../inequality-rational-numbers.lagda.md | 15 +- ...closed-intervals-rational-numbers.lagda.md | 16 +- ...ication-positive-rational-numbers.lagda.md | 2 +- .../negative-rational-numbers.lagda.md | 4 +- .../positive-rational-numbers.lagda.md | 2 +- ...e-roots-positive-rational-numbers.lagda.md | 22 +- ...trict-inequality-rational-numbers.lagda.md | 33 +- .../metrics-of-metric-spaces.lagda.md | 8 +- src/metric-spaces/metrics.lagda.md | 12 +- src/real-numbers.lagda.md | 7 + ...lue-closed-intervals-real-numbers.lagda.md | 2 +- .../absolute-value-real-numbers.lagda.md | 26 +- ...ition-lower-dedekind-real-numbers.lagda.md | 2 +- ...addition-nonnegative-real-numbers.lagda.md | 136 ++++++++ ...ition-upper-dedekind-real-numbers.lagda.md | 2 +- ...thmetically-located-dedekind-cuts.lagda.md | 20 +- .../binary-maximum-real-numbers.lagda.md | 23 +- .../binary-minimum-real-numbers.lagda.md | 13 +- ...ompleteness-dedekind-real-numbers.lagda.md | 13 +- .../closed-intervals-real-numbers.lagda.md | 6 +- .../dedekind-real-numbers.lagda.md | 8 +- .../distance-real-numbers.lagda.md | 6 +- ...nequalities-addition-real-numbers.lagda.md | 234 +++++++++++++ ...equality-nonnegative-real-numbers.lagda.md | 159 +++++++++ .../inequality-real-numbers.lagda.md | 267 ++------------- .../infima-families-real-numbers.lagda.md | 17 +- ...ally-bounded-subsets-real-numbers.lagda.md | 11 +- .../isometry-addition-real-numbers.lagda.md | 1 + .../isometry-negation-real-numbers.lagda.md | 29 ++ ...nuity-multiplication-real-numbers.lagda.md | 27 +- ...imum-finite-families-real-numbers.lagda.md | 1 + ...space-of-nonnegative-real-numbers.lagda.md | 34 ++ .../metric-space-of-real-numbers.lagda.md | 21 +- ...tiplication-negative-real-numbers.lagda.md | 4 +- ...lication-nonnegative-real-numbers.lagda.md | 5 +- .../multiplication-real-numbers.lagda.md | 12 +- ...ve-inverses-positive-real-numbers.lagda.md | 3 +- .../negation-real-numbers.lagda.md | 2 +- .../nonnegative-real-numbers.lagda.md | 319 +---------------- ...ositive-and-negative-real-numbers.lagda.md | 6 +- .../positive-real-numbers.lagda.md | 39 +-- ...sing-universe-levels-real-numbers.lagda.md | 2 +- .../rational-real-numbers.lagda.md | 14 +- ...equality-nonnegative-real-numbers.lagda.md | 71 ++++ ...aturation-inequality-real-numbers.lagda.md | 29 +- ...milarity-nonnegative-real-numbers.lagda.md | 70 ++++ ...re-roots-nonnegative-real-numbers.lagda.md | 9 +- .../squares-real-numbers.lagda.md | 10 +- ...nequalities-addition-real-numbers.lagda.md | 289 ++++++++++++++++ ...equality-nonnegative-real-numbers.lagda.md | 42 ++- .../strict-inequality-real-numbers.lagda.md | 323 ++---------------- .../suprema-families-real-numbers.lagda.md | 5 +- ...action-cuts-dedekind-real-numbers.lagda.md | 13 +- 56 files changed, 1340 insertions(+), 1126 deletions(-) create mode 100644 src/real-numbers/addition-nonnegative-real-numbers.lagda.md create mode 100644 src/real-numbers/inequalities-addition-real-numbers.lagda.md create mode 100644 src/real-numbers/inequality-nonnegative-real-numbers.lagda.md create mode 100644 src/real-numbers/metric-space-of-nonnegative-real-numbers.lagda.md create mode 100644 src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md create mode 100644 src/real-numbers/similarity-nonnegative-real-numbers.lagda.md create mode 100644 src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md diff --git a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md index 4b0ad01d88..031a23160f 100644 --- a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md +++ b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md @@ -166,7 +166,7 @@ abstract ( q) ( rational-abs-ℚ q) ( zero-ℚ) - ( leq-eq-ℚ _ _ (ap rational-ℚ⁰⁺ abs=0)) + ( leq-eq-ℚ (ap rational-ℚ⁰⁺ abs=0)) ( leq-abs-ℚ q)) ( binary-tr ( leq-ℚ) 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 85668704af..7e1cf13e5b 100644 --- a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md @@ -169,7 +169,7 @@ module _ where le-diff-ℚ⁺ : ℚ⁺ - le-diff-ℚ⁺ = positive-diff-le-ℚ (rational-ℚ⁺ x) (rational-ℚ⁺ y) H + le-diff-ℚ⁺ = positive-diff-le-ℚ H left-diff-law-add-ℚ⁺ : le-diff-ℚ⁺ +ℚ⁺ x = y left-diff-law-add-ℚ⁺ = @@ -342,15 +342,8 @@ module _ ( le-right-mediant-ℚ y x I) ( tr ( leq-ℚ x) - ( right-law-positive-diff-le-ℚ - ( y) - ( mediant-ℚ y x) - ( le-left-mediant-ℚ y x I)) - ( H - ( positive-diff-le-ℚ - ( y) - ( mediant-ℚ y x) - ( le-left-mediant-ℚ y x I)))))) + ( right-law-positive-diff-le-ℚ (le-left-mediant-ℚ y x I)) + ( H (positive-diff-le-ℚ (le-left-mediant-ℚ y x I)))))) ( id) ( decide-le-leq-ℚ y x) diff --git a/src/elementary-number-theory/distance-rational-numbers.lagda.md b/src/elementary-number-theory/distance-rational-numbers.lagda.md index 6a9bcc3d5d..3926d248dc 100644 --- a/src/elementary-number-theory/distance-rational-numbers.lagda.md +++ b/src/elementary-number-theory/distance-rational-numbers.lagda.md @@ -191,10 +191,7 @@ abstract ( rational-dist-ℚ p q) ( (rational-abs-ℚ p) +ℚ (rational-abs-ℚ (neg-ℚ q))) ( rational-abs-ℚ p +ℚ rational-abs-ℚ q) - ( leq-eq-ℚ - ( (rational-abs-ℚ p) +ℚ (rational-abs-ℚ (neg-ℚ q))) - ( rational-abs-ℚ p +ℚ rational-abs-ℚ q) - ( ap (add-ℚ (rational-abs-ℚ p) ∘ rational-ℚ⁰⁺) (abs-neg-ℚ q))) + ( leq-eq-ℚ (ap (add-ℚ (rational-abs-ℚ p) ∘ rational-ℚ⁰⁺) (abs-neg-ℚ q))) ( triangle-inequality-abs-ℚ p (neg-ℚ q)) ``` diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md index 14d1a9398e..29d6fb57a9 100644 --- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md @@ -126,8 +126,8 @@ opaque refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x) abstract - leq-eq-ℚ : (x y : ℚ) → x = y → leq-ℚ x y - leq-eq-ℚ x y x=y = tr (leq-ℚ x) x=y (refl-leq-ℚ x) + leq-eq-ℚ : {x y : ℚ} → x = y → leq-ℚ x y + leq-eq-ℚ {x} refl = refl-leq-ℚ x ``` ### Inequality on the rational numbers is antisymmetric @@ -294,8 +294,8 @@ opaque unfolding leq-ℚ-Prop preserves-leq-rational-ℤ : - (x y : ℤ) → leq-ℤ x y → leq-ℚ (rational-ℤ x) (rational-ℤ y) - preserves-leq-rational-ℤ x y = + {x y : ℤ} → leq-ℤ x y → leq-ℚ (rational-ℤ x) (rational-ℤ y) + preserves-leq-rational-ℤ {x} {y} = binary-tr leq-ℤ ( inv (right-unit-law-mul-ℤ x)) ( inv (right-unit-law-mul-ℤ y)) @@ -309,7 +309,7 @@ opaque iff-leq-rational-ℤ : (x y : ℤ) → leq-ℤ x y ↔ leq-ℚ (rational-ℤ x) (rational-ℤ y) - pr1 (iff-leq-rational-ℤ x y) = preserves-leq-rational-ℤ x y + pr1 (iff-leq-rational-ℤ x y) = preserves-leq-rational-ℤ pr2 (iff-leq-rational-ℤ x y) = reflects-leq-rational-ℤ x y ``` @@ -324,8 +324,9 @@ abstract iff-leq-int-ℕ x y preserves-leq-rational-ℕ : - (x y : ℕ) → leq-ℕ x y → leq-ℚ (rational-ℕ x) (rational-ℕ y) - preserves-leq-rational-ℕ x y = forward-implication (iff-leq-rational-ℕ x y) + {x y : ℕ} → leq-ℕ x y → leq-ℚ (rational-ℕ x) (rational-ℕ y) + preserves-leq-rational-ℕ {x} {y} = + forward-implication (iff-leq-rational-ℕ x y) reflects-leq-rational-ℕ : (x y : ℕ) → leq-ℚ (rational-ℕ x) (rational-ℕ y) → leq-ℕ x y diff --git a/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md index 8ec9ae546c..698a8adb82 100644 --- a/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md @@ -924,7 +924,7 @@ abstract rational-dist-ℚ (a *ℚ q) (b *ℚ q) ≤ rational-dist-ℚ a b *ℚ rational-abs-ℚ q by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ( ap ( rational-abs-ℚ) ( inv (right-distributive-mul-diff-ℚ _ _ _))) ∙ @@ -939,7 +939,7 @@ abstract ≤ width-closed-interval-ℚ [a,b] *ℚ rational-max-abs-closed-interval-ℚ [c,d] by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ap-mul-ℚ ( eq-width-dist-lower-upper-bounds-closed-interval-ℚ [a,b]) ( refl)) @@ -951,7 +951,7 @@ abstract rational-dist-ℚ (p *ℚ c) (p *ℚ d) ≤ rational-dist-ℚ c d *ℚ rational-abs-ℚ p by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ( ap ( rational-abs-ℚ) ( inv (left-distributive-mul-diff-ℚ _ _ _))) ∙ @@ -966,7 +966,7 @@ abstract ( leq-max-abs-is-in-closed-interval-ℚ [a,b] p p∈[a,b]) ≤ _ by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ap-mul-ℚ ( eq-width-dist-lower-upper-bounds-closed-interval-ℚ [c,d]) ( refl)) @@ -983,7 +983,7 @@ abstract rational-dist-ℚ (a *ℚ c) (b *ℚ d) ≤ rational-abs-ℚ ((a *ℚ c -ℚ b *ℚ c) +ℚ (b *ℚ c -ℚ b *ℚ d)) by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ap ( rational-abs-ℚ) ( inv ( mul-right-div-Group group-add-ℚ _ _ _))) @@ -996,7 +996,7 @@ abstract rational-dist-ℚ (a *ℚ d) (b *ℚ c) ≤ rational-abs-ℚ ((a *ℚ d -ℚ b *ℚ d) +ℚ (b *ℚ d -ℚ b *ℚ c)) by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ap ( rational-abs-ℚ) ( inv ( mul-right-div-Group group-add-ℚ _ _ _))) @@ -1006,7 +1006,7 @@ abstract ≤ rational-dist-ℚ (a *ℚ d) (b *ℚ d) +ℚ rational-dist-ℚ (b *ℚ c) (b *ℚ d) by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ap-add-ℚ refl (ap rational-ℚ⁰⁺ (commutative-dist-ℚ _ _))) ≤ +ℚ by preserves-leq-add-ℚ |ad-bd|≤max|c||d| |bc-bd|≤max|a||b| @@ -1042,7 +1042,7 @@ abstract chain-of-inequalities rational-dist-ℚ q q ≤ zero-ℚ - by leq-eq-ℚ _ _ (rational-dist-self-ℚ q) + by leq-eq-ℚ (rational-dist-self-ℚ q) ≤ +ℚ by leq-zero-rational-ℚ⁰⁺ (⁰⁺ +ℚ⁰⁺ ⁰⁺) diff --git a/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md index e0fb4cbbe4..492703832c 100644 --- a/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md @@ -357,6 +357,6 @@ abstract leq-left-mul-leq-one-ℚ⁺ p⁺@(p , _) p≤1 q⁺@(q , _) = trichotomy-le-ℚ p one-ℚ ( λ p<1 → leq-le-ℚ (le-left-mul-less-than-one-ℚ⁺ p⁺ p<1 q⁺)) - ( λ p=1 → leq-eq-ℚ _ _ (ap-mul-ℚ p=1 refl ∙ left-unit-law-mul-ℚ q)) + ( λ p=1 → leq-eq-ℚ (ap-mul-ℚ p=1 refl ∙ left-unit-law-mul-ℚ q)) ( λ 1

Imports + +```agda +open import elementary-number-theory.addition-nonnegative-rational-numbers +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.inequalities-addition-real-numbers +open import real-numbers.inequality-nonnegative-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequalities-addition-real-numbers +open import real-numbers.strict-inequality-nonnegative-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + + + +## Idea + +The [nonnegative](real-numbers.nonnegative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are closed under +[addition](real-numbers.addition-real-numbers.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) + where + + real-add-ℝ⁰⁺ : ℝ (l1 ⊔ l2) + real-add-ℝ⁰⁺ = real-ℝ⁰⁺ x +ℝ real-ℝ⁰⁺ y + + abstract + is-nonnegative-real-add-ℝ⁰⁺ : is-nonnegative-ℝ real-add-ℝ⁰⁺ + is-nonnegative-real-add-ℝ⁰⁺ = + tr + ( λ z → leq-ℝ z (real-ℝ⁰⁺ x +ℝ real-ℝ⁰⁺ y)) + ( left-unit-law-add-ℝ zero-ℝ) + ( preserves-leq-add-ℝ + ( is-nonnegative-real-ℝ⁰⁺ x) + ( is-nonnegative-real-ℝ⁰⁺ y)) + + add-ℝ⁰⁺ : ℝ⁰⁺ (l1 ⊔ l2) + add-ℝ⁰⁺ = (real-add-ℝ⁰⁺ , is-nonnegative-real-add-ℝ⁰⁺) + +infixl 35 _+ℝ⁰⁺_ + +_+ℝ⁰⁺_ : {l1 l2 : Level} → ℝ⁰⁺ l1 → ℝ⁰⁺ l2 → ℝ⁰⁺ (l1 ⊔ l2) +_+ℝ⁰⁺_ = add-ℝ⁰⁺ +``` + +## Properties + +### Unit laws for addition + +```agda +module _ + {l : Level} (x : ℝ⁰⁺ l) + where + + abstract + left-unit-law-add-ℝ⁰⁺ : zero-ℝ⁰⁺ +ℝ⁰⁺ x = x + left-unit-law-add-ℝ⁰⁺ = eq-ℝ⁰⁺ _ _ (left-unit-law-add-ℝ _) + + right-unit-law-add-ℝ⁰⁺ : x +ℝ⁰⁺ zero-ℝ⁰⁺ = x + right-unit-law-add-ℝ⁰⁺ = eq-ℝ⁰⁺ _ _ (right-unit-law-add-ℝ _) +``` + +### Addition preserves inequality + +```agda +module _ + {l1 l2 l3 l4 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) (z : ℝ⁰⁺ l3) (w : ℝ⁰⁺ l4) + where + + abstract + preserves-leq-add-ℝ⁰⁺ : + leq-ℝ⁰⁺ x y → leq-ℝ⁰⁺ z w → leq-ℝ⁰⁺ (x +ℝ⁰⁺ z) (y +ℝ⁰⁺ w) + preserves-leq-add-ℝ⁰⁺ = preserves-leq-add-ℝ +``` + +### The canonical embedding of nonnegative rational numbers to nonnegative real numbers preserves addition + +```agda +abstract + add-nonnegative-real-ℚ⁰⁺ : + (p q : ℚ⁰⁺) → + nonnegative-real-ℚ⁰⁺ p +ℝ⁰⁺ nonnegative-real-ℚ⁰⁺ q = + nonnegative-real-ℚ⁰⁺ (p +ℚ⁰⁺ q) + add-nonnegative-real-ℚ⁰⁺ p q = + eq-ℝ⁰⁺ _ _ (add-real-ℚ (rational-ℚ⁰⁺ p) (rational-ℚ⁰⁺ q)) +``` + +### The canonical embedding of positive rational numbers to nonnegative real numbers preserves addition + +```agda +abstract + add-nonnegative-real-ℚ⁺ : + (p q : ℚ⁺) → + nonnegative-real-ℚ⁺ p +ℝ⁰⁺ nonnegative-real-ℚ⁺ q = + nonnegative-real-ℚ⁺ (p +ℚ⁺ q) + add-nonnegative-real-ℚ⁺ p q = + eq-ℝ⁰⁺ _ _ (add-real-ℚ (rational-ℚ⁺ p) (rational-ℚ⁺ q)) +``` + +### Addition preserves strict inequality + +```agda +module _ + {l1 l2 l3 l4 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) (z : ℝ⁰⁺ l3) (w : ℝ⁰⁺ l4) + where + + abstract + preserves-le-add-ℝ⁰⁺ : + le-ℝ⁰⁺ x y → le-ℝ⁰⁺ z w → le-ℝ⁰⁺ (x +ℝ⁰⁺ z) (y +ℝ⁰⁺ w) + preserves-le-add-ℝ⁰⁺ = preserves-le-add-ℝ +``` diff --git a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md index 44bd7f51ae..616124b951 100644 --- a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md @@ -111,7 +111,7 @@ module _ (p , pImports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types +open import foundation.logical-equivalences +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +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.inequality-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.rational-real-numbers +``` + + + +## Idea + +This file describes lemmas about +[inequalities](real-numbers.inequality-real-numbers.md) of +[real numbers](real-numbers.dedekind-real-numbers.md) related to +[addition](real-numbers.addition-real-numbers.md) and +[subtraction](real-numbers.difference-real-numbers.md). + +## Lemmas + +### Inequality on the real numbers is translation invariant + +```agda +module _ + {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) + where + + opaque + unfolding add-ℝ leq-ℝ + + preserves-leq-right-add-ℝ : leq-ℝ x y → leq-ℝ (x +ℝ z) (y +ℝ z) + preserves-leq-right-add-ℝ x≤y _ = + map-tot-exists (λ (qx , _) → map-product (x≤y qx) id) + + preserves-leq-left-add-ℝ : leq-ℝ x y → leq-ℝ (z +ℝ x) (z +ℝ y) + preserves-leq-left-add-ℝ x≤y _ = + map-tot-exists (λ (_ , qx) → map-product id (map-product (x≤y qx) id)) + +abstract + preserves-leq-diff-ℝ : + {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) → + leq-ℝ x y → leq-ℝ (x -ℝ z) (y -ℝ z) + preserves-leq-diff-ℝ z = preserves-leq-right-add-ℝ (neg-ℝ z) + +module _ + {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) + where + + abstract + reflects-leq-right-add-ℝ : leq-ℝ (x +ℝ z) (y +ℝ z) → leq-ℝ x y + reflects-leq-right-add-ℝ x+z≤y+z = + preserves-leq-sim-ℝ + ( (x +ℝ z) -ℝ z) + ( x) + ( (y +ℝ z) -ℝ z) + ( y) + ( cancel-right-add-diff-ℝ x z) + ( cancel-right-add-diff-ℝ y z) + ( preserves-leq-right-add-ℝ (neg-ℝ z) (x +ℝ z) (y +ℝ z) x+z≤y+z) + + reflects-leq-left-add-ℝ : leq-ℝ (z +ℝ x) (z +ℝ y) → leq-ℝ x y + reflects-leq-left-add-ℝ z+x≤z+y = + reflects-leq-right-add-ℝ + ( binary-tr + ( leq-ℝ) + ( commutative-add-ℝ z x) + ( commutative-add-ℝ z y) + ( z+x≤z+y)) + +module _ + {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) + where + + iff-translate-right-leq-ℝ : leq-ℝ x y ↔ leq-ℝ (x +ℝ z) (y +ℝ z) + pr1 iff-translate-right-leq-ℝ = preserves-leq-right-add-ℝ z x y + pr2 iff-translate-right-leq-ℝ = reflects-leq-right-add-ℝ z x y + + iff-translate-left-leq-ℝ : leq-ℝ x y ↔ leq-ℝ (z +ℝ x) (z +ℝ y) + pr1 iff-translate-left-leq-ℝ = preserves-leq-left-add-ℝ z x y + pr2 iff-translate-left-leq-ℝ = reflects-leq-left-add-ℝ z x y + +abstract + preserves-leq-add-ℝ : + {l1 l2 l3 l4 : Level} {a : ℝ l1} {b : ℝ l2} {c : ℝ l3} {d : ℝ l4} → + leq-ℝ a b → leq-ℝ c d → leq-ℝ (a +ℝ c) (b +ℝ d) + preserves-leq-add-ℝ {a = a} {b = b} {c = c} {d = d} a≤b c≤d = + transitive-leq-ℝ + ( a +ℝ c) + ( a +ℝ d) + ( b +ℝ d) + ( preserves-leq-right-add-ℝ d a b a≤b) + ( preserves-leq-left-add-ℝ a c d c≤d) +``` + +### Transposition laws + +```agda +module _ + {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) + where + + abstract + leq-transpose-left-diff-ℝ : leq-ℝ (x -ℝ y) z → leq-ℝ x (z +ℝ y) + leq-transpose-left-diff-ℝ x-y≤z = + preserves-leq-left-sim-ℝ + ( cancel-right-diff-add-ℝ x y) + ( preserves-leq-right-add-ℝ y (x -ℝ y) z x-y≤z) + + leq-transpose-left-add-ℝ : leq-ℝ (x +ℝ y) z → leq-ℝ x (z -ℝ y) + leq-transpose-left-add-ℝ x+y≤z = + preserves-leq-left-sim-ℝ + ( cancel-right-add-diff-ℝ x y) + ( preserves-leq-right-add-ℝ (neg-ℝ y) (x +ℝ y) z x+y≤z) + + leq-transpose-right-add-ℝ : leq-ℝ x (y +ℝ z) → leq-ℝ (x -ℝ z) y + leq-transpose-right-add-ℝ x≤y+z = + preserves-leq-right-sim-ℝ + ( cancel-right-add-diff-ℝ y z) + ( preserves-leq-right-add-ℝ (neg-ℝ z) x (y +ℝ z) x≤y+z) + + leq-transpose-right-diff-ℝ : leq-ℝ x (y -ℝ z) → leq-ℝ (x +ℝ z) y + leq-transpose-right-diff-ℝ x≤y-z = + preserves-leq-right-sim-ℝ + ( cancel-right-diff-add-ℝ y z) + ( preserves-leq-right-add-ℝ z x (y -ℝ z) x≤y-z) +``` + +### Swapping laws + +```agda +abstract + swap-right-diff-leq-ℝ : + {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) → + leq-ℝ (x -ℝ y) z → leq-ℝ (x -ℝ z) y + swap-right-diff-leq-ℝ x y z x-y≤z = + leq-transpose-right-add-ℝ + ( x) + ( y) + ( z) + ( tr + ( leq-ℝ x) + ( commutative-add-ℝ _ _) + ( leq-transpose-left-diff-ℝ x y z x-y≤z)) +``` + +### Addition of real numbers preserves lower neighborhoods + +```agda +module _ + {l1 l2 l3 : Level} (d : ℚ⁺) + (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) + where + + abstract + preserves-lower-neighborhood-leq-left-add-ℝ : + leq-ℝ y (z +ℝ real-ℚ⁺ d) → + leq-ℝ (x +ℝ y) ((x +ℝ z) +ℝ real-ℚ⁺ d) + preserves-lower-neighborhood-leq-left-add-ℝ z≤y+d = + inv-tr + ( leq-ℝ (x +ℝ y)) + ( associative-add-ℝ x z (real-ℚ⁺ d)) + ( preserves-leq-left-add-ℝ + ( x) + ( y) + ( z +ℝ real-ℚ⁺ d) + ( z≤y+d)) + + preserves-lower-neighborhood-leq-right-add-ℝ : + leq-ℝ y (z +ℝ real-ℚ⁺ d) → + leq-ℝ (y +ℝ x) ((z +ℝ x) +ℝ real-ℚ⁺ d) + preserves-lower-neighborhood-leq-right-add-ℝ z≤y+d = + binary-tr + ( λ u v → leq-ℝ u (v +ℝ real-ℚ⁺ d)) + ( commutative-add-ℝ x y) + ( commutative-add-ℝ x z) + ( preserves-lower-neighborhood-leq-left-add-ℝ z≤y+d) +``` + +### Addition of real numbers reflects lower neighborhoods + +```agda +module _ + {l1 l2 l3 : Level} (d : ℚ⁺) + (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) + where + + abstract + reflects-lower-neighborhood-leq-left-add-ℝ : + leq-ℝ (x +ℝ y) ((x +ℝ z) +ℝ real-ℚ⁺ d) → + leq-ℝ y (z +ℝ real-ℚ⁺ d) + reflects-lower-neighborhood-leq-left-add-ℝ x+y≤x+z+d = + reflects-leq-left-add-ℝ + ( x) + ( y) + ( z +ℝ real-ℚ⁺ d) + ( tr + ( leq-ℝ (x +ℝ y)) + ( associative-add-ℝ x z (real-ℚ⁺ d)) + ( x+y≤x+z+d)) + + reflects-lower-neighborhood-leq-right-add-ℝ : + leq-ℝ (y +ℝ x) ((z +ℝ x) +ℝ real-ℚ⁺ d) → + leq-ℝ y (z +ℝ real-ℚ⁺ d) + reflects-lower-neighborhood-leq-right-add-ℝ y+x≤z+y+d = + reflects-lower-neighborhood-leq-left-add-ℝ + ( binary-tr + ( λ u v → leq-ℝ u (v +ℝ real-ℚ⁺ d)) + ( commutative-add-ℝ y x) + ( commutative-add-ℝ z x) + ( y+x≤z+y+d)) +``` diff --git a/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md b/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md new file mode 100644 index 0000000000..fa71aea44a --- /dev/null +++ b/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md @@ -0,0 +1,159 @@ +# Inequality of nonnegative real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.inequality-nonnegative-real-numbers where +``` + +
Imports + +```agda +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.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.function-types +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-nonnegative-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +The +{{#concept "standard ordering" Disambiguation="on the nonnegative real numbers" Agda=leq-ℝ⁰⁺}} +on the [nonnegative real numbers](real-numbers.nonnegative-real-numbers.md) is +inherited from the [standard ordering](real-numbers.inequality-real-numbers.md) +on [real numbers](real-numbers.dedekind-real-numbers.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) + where + + leq-prop-ℝ⁰⁺ : Prop (l1 ⊔ l2) + leq-prop-ℝ⁰⁺ = leq-prop-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) + + leq-ℝ⁰⁺ : UU (l1 ⊔ l2) + leq-ℝ⁰⁺ = type-Prop leq-prop-ℝ⁰⁺ +``` + +## Properties + +### Zero is less than or equal to every nonnegative real number + +```agda +leq-zero-ℝ⁰⁺ : {l : Level} (x : ℝ⁰⁺ l) → leq-ℝ⁰⁺ zero-ℝ⁰⁺ x +leq-zero-ℝ⁰⁺ = is-nonnegative-real-ℝ⁰⁺ +``` + +### Similarity preserves inequality + +```agda +module _ + {l1 l2 l3 : Level} (z : ℝ⁰⁺ l1) (x : ℝ⁰⁺ l2) (y : ℝ⁰⁺ l3) (x~y : sim-ℝ⁰⁺ x y) + where + + abstract + preserves-leq-left-sim-ℝ⁰⁺ : leq-ℝ⁰⁺ x z → leq-ℝ⁰⁺ y z + preserves-leq-left-sim-ℝ⁰⁺ = preserves-leq-left-sim-ℝ x~y +``` + +### Inequality is transitive + +```agda +module _ + {l1 l2 l3 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) (z : ℝ⁰⁺ l3) + where + + transitive-leq-ℝ⁰⁺ : leq-ℝ⁰⁺ y z → leq-ℝ⁰⁺ x y → leq-ℝ⁰⁺ x z + transitive-leq-ℝ⁰⁺ = transitive-leq-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) (real-ℝ⁰⁺ z) +``` + +### If `x` is less than all the positive rational numbers `y` is less than, then `x ≤ y` + +```agda +module _ + {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) + where + + abstract + leq-le-positive-rational-ℝ⁰⁺ : + ( (q : ℚ⁺) → le-ℝ (real-ℝ⁰⁺ y) (real-ℚ⁺ q) → + le-ℝ (real-ℝ⁰⁺ x) (real-ℚ⁺ q)) → + leq-ℝ⁰⁺ x y + leq-le-positive-rational-ℝ⁰⁺ H = + leq-le-rational-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) + ( λ q y @@ -36,6 +41,30 @@ open import real-numbers.negation-real-numbers ## Definitions +### Negation of real numbers reverses lower neighborhoods + +```agda +module _ + {l1 l2 : Level} (d : ℚ⁺) + (x : ℝ l1) (y : ℝ l2) + where + + reverses-lower-neighborhood-neg-ℝ : + leq-ℝ x (y +ℝ real-ℚ⁺ d) → + leq-ℝ (neg-ℝ y) (neg-ℝ x +ℝ real-ℚ⁺ d) + reverses-lower-neighborhood-neg-ℝ x≤y+d = + tr + ( leq-ℝ (neg-ℝ y)) + ( ( distributive-neg-add-ℝ x ((neg-ℝ ∘ real-ℚ ∘ rational-ℚ⁺) d)) ∙ + ( ap (add-ℝ (neg-ℝ x)) (neg-neg-ℝ (real-ℚ⁺ d)))) + ( neg-leq-ℝ + ( leq-transpose-right-add-ℝ + ( x) + ( y) + ( real-ℚ⁺ d) + ( x≤y+d))) +``` + ### Negation of a real number preserves neighborhoods ```agda diff --git a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md index 9e1a1f4786..7b3d8f8c66 100644 --- a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md +++ b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md @@ -30,11 +30,13 @@ open import order-theory.large-posets open import real-numbers.absolute-value-closed-intervals-real-numbers open import real-numbers.absolute-value-real-numbers +open import real-numbers.addition-nonnegative-real-numbers open import real-numbers.addition-real-numbers open import real-numbers.arithmetically-located-dedekind-cuts open import real-numbers.dedekind-real-numbers open import real-numbers.distance-real-numbers open import real-numbers.enclosing-closed-rational-intervals-real-numbers +open import real-numbers.inequalities-addition-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.inhabited-totally-bounded-subsets-real-numbers open import real-numbers.metric-space-of-real-numbers @@ -90,7 +92,7 @@ module _ ( chain-of-inequalities dist-ℝ (c *ℝ x) (c *ℝ y) ≤ abs-ℝ c *ℝ dist-ℝ x y - by leq-eq-ℝ _ _ (inv (left-distributive-abs-mul-dist-ℝ _ _ _)) + by leq-eq-ℝ (inv (left-distributive-abs-mul-dist-ℝ _ _ _)) ≤ real-ℚ⁺ q *ℝ real-ℚ⁺ ε by preserves-leq-mul-ℝ⁰⁺ @@ -98,14 +100,10 @@ module _ ( nonnegative-real-ℚ⁺ q) ( nonnegative-dist-ℝ x y) ( nonnegative-real-ℚ⁺ ε) - ( leq-le-ℝ _ _ - ( le-real-is-in-upper-cut-ℚ - ( rational-ℚ⁺ q) - ( abs-ℝ c) - ( |c|Imports + +```agda +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.nonnegative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) form a +[subspace](metric-spaces.subspaces-metric-spaces.md) of the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). + +## Definition + +```agda +metric-space-ℝ⁰⁺ : (l : Level) → Metric-Space (lsuc l) l +metric-space-ℝ⁰⁺ l = metric-space-subset-ℝ (is-nonnegative-prop-ℝ {l}) +``` 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 9c80701de0..5afe6b7b56 100644 --- a/src/real-numbers/metric-space-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-space-of-real-numbers.lagda.md @@ -44,10 +44,12 @@ open import metric-spaces.triangular-rational-neighborhood-relations 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-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequalities-addition-real-numbers open import real-numbers.strict-inequality-real-numbers open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers ``` @@ -170,15 +172,11 @@ module _ elim-exists ( lower-cut-ℝ x r) ( λ r' (K , I') → - H ( positive-diff-le-ℚ (r +ℚ rational-ℚ⁺ ε) r' K) + H ( positive-diff-le-ℚ K) ( r) ( tr ( is-in-lower-cut-ℝ y) - ( ( inv - ( right-law-positive-diff-le-ℚ - ( r +ℚ rational-ℚ⁺ ε) - ( r') - ( K))) ∙ + ( ( inv (right-law-positive-diff-le-ℚ K)) ∙ ( associative-add-ℚ ( r) ( rational-ℚ⁺ ε) @@ -221,11 +219,11 @@ module _ ( lower-cut-ℝ y r) ( λ s (rImports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.addition-nonnegative-real-numbers +open import real-numbers.inequality-nonnegative-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.saturation-inequality-real-numbers +open import real-numbers.similarity-nonnegative-real-numbers +``` + + + +## Idea + +If `x ≤ y + ε` for [nonnegative](real-numbers.nonnegative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) `x` and `y` and every +[positive rational](elementary-number-theory.positive-rational-numbers.md) `ε`, +then `x ≤ y`. + +Despite being a property of +[inequality of nonnegative real numbers](real-numbers.inequality-nonnegative-real-numbers.md), +this is much easier to prove via +[strict inequality](real-numbers.strict-inequality-nonnegative-real-numbers.md), +so it is moved to its own file to prevent circular dependency. + +## Definition + +```agda +module _ + {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) + where + + abstract + saturated-leq-ℝ⁰⁺ : + ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (y +ℝ⁰⁺ nonnegative-real-ℚ⁺ ε)) → + leq-ℝ⁰⁺ x y + saturated-leq-ℝ⁰⁺ = saturated-leq-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) +``` + +## Corollaries + +### If a nonnegative real number is less than or equal to all positive rational numbers, it is similar to zero + +```agda +sim-zero-le-positive-rational-ℝ⁰⁺ : + {l : Level} (x : ℝ⁰⁺ l) → + ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (nonnegative-real-ℚ⁺ ε)) → + sim-zero-ℝ⁰⁺ x +sim-zero-le-positive-rational-ℝ⁰⁺ x H = + sim-sim-leq-ℝ + ( leq-zero-ℝ⁰⁺ x , + saturated-leq-ℝ⁰⁺ + ( x) + ( zero-ℝ⁰⁺) + ( λ ε → inv-tr (leq-ℝ⁰⁺ x) (left-unit-law-add-ℝ⁰⁺ _) (H ε))) +``` diff --git a/src/real-numbers/saturation-inequality-real-numbers.lagda.md b/src/real-numbers/saturation-inequality-real-numbers.lagda.md index 6657f97f72..437a1a7a32 100644 --- a/src/real-numbers/saturation-inequality-real-numbers.lagda.md +++ b/src/real-numbers/saturation-inequality-real-numbers.lagda.md @@ -12,12 +12,16 @@ module real-numbers.saturation-inequality-real-numbers where open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.strict-inequality-positive-rational-numbers +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.propositional-truncations open import foundation.universe-levels open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequalities-addition-real-numbers open import real-numbers.strict-inequality-real-numbers ``` @@ -38,6 +42,29 @@ moved to its own file to prevent circular dependency. ## Proof +### If `x < y + ε` for every positive rational `ε`, then `x ≤ y` + +```agda +module _ + {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) + where + + abstract + saturated-le-ℝ : ((ε : ℚ⁺) → le-ℝ x (y +ℝ real-ℚ⁺ ε)) → leq-ℝ x y + saturated-le-ℝ H = + leq-not-le-ℝ y x + ( λ yImports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositions +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + + + +## Idea + +Two [nonnegative](real-numbers.nonnegative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are +{{#concept "similar" Disambiguation="nonnegative real numbers" Agda=sim-ℝ⁰⁺}} if +they are [similar](real-numbers.similarity-real-numbers.md) as real numbers. + +## Definition + +### Similarity of nonnegative real numbers + +```agda +module _ + {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) + where + + sim-prop-ℝ⁰⁺ : Prop (l1 ⊔ l2) + sim-prop-ℝ⁰⁺ = sim-prop-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) + + sim-ℝ⁰⁺ : UU (l1 ⊔ l2) + sim-ℝ⁰⁺ = sim-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) + +infix 6 _~ℝ⁰⁺_ +_~ℝ⁰⁺_ : {l1 l2 : Level} → ℝ⁰⁺ l1 → ℝ⁰⁺ l2 → UU (l1 ⊔ l2) +_~ℝ⁰⁺_ = sim-ℝ⁰⁺ + +sim-zero-prop-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → Prop l +sim-zero-prop-ℝ⁰⁺ = sim-prop-ℝ⁰⁺ zero-ℝ⁰⁺ + +sim-zero-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → UU l +sim-zero-ℝ⁰⁺ = sim-ℝ⁰⁺ zero-ℝ⁰⁺ + +eq-sim-ℝ⁰⁺ : {l : Level} (x y : ℝ⁰⁺ l) → sim-ℝ⁰⁺ x y → x = y +eq-sim-ℝ⁰⁺ x y x~y = eq-ℝ⁰⁺ x y (eq-sim-ℝ {x = real-ℝ⁰⁺ x} {y = real-ℝ⁰⁺ y} x~y) +``` + +#### Similarity is symmetric + +```agda +abstract + symmetric-sim-ℝ⁰⁺ : + {l1 l2 : Level} → (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) → x ~ℝ⁰⁺ y → y ~ℝ⁰⁺ x + symmetric-sim-ℝ⁰⁺ _ _ = symmetric-sim-ℝ +``` diff --git a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md index a9576b242d..154237168d 100644 --- a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md @@ -54,6 +54,7 @@ open import real-numbers.multiplication-nonnegative-real-numbers open import real-numbers.multiplication-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.rational-real-numbers +open import real-numbers.similarity-nonnegative-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.squares-real-numbers ``` @@ -184,7 +185,7 @@ module _ (p , pImports + +```agda +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.difference-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.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.addition-real-numbers +open import real-numbers.arithmetically-located-dedekind-cuts +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.negation-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + + + +## Idea + +This file describes lemmas about +[strict inequalities](real-numbers.strict-inequality-real-numbers.md) of +[real numbers](real-numbers.dedekind-real-numbers.md) related to +[addition](real-numbers.addition-real-numbers.md) and +[subtraction](real-numbers.difference-real-numbers.md). + +## Lemmas + +### Strict inequality on the real numbers is translation invariant + +```agda +module _ + {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) + where + + opaque + unfolding add-ℝ le-ℝ + + preserves-le-right-add-ℝ : le-ℝ x y → le-ℝ (x +ℝ z) (y +ℝ z) + preserves-le-right-add-ℝ x Date: Fri, 7 Nov 2025 15:01:52 -0800 Subject: [PATCH 02/21] Progress --- ...lue-closed-intervals-real-numbers.lagda.md | 2 -- .../absolute-value-real-numbers.lagda.md | 16 +++------ .../distance-real-numbers.lagda.md | 16 ++++----- ...nequalities-addition-real-numbers.lagda.md | 4 --- .../inequality-real-numbers.lagda.md | 2 +- .../metric-space-of-real-numbers.lagda.md | 8 ----- ...tiplication-positive-real-numbers.lagda.md | 4 +-- .../nonnegative-real-numbers.lagda.md | 27 ++++++++------- .../positive-real-numbers.lagda.md | 4 +-- .../similarity-positive-real-numbers.lagda.md | 34 +++++++++++++++++++ ...nequalities-addition-real-numbers.lagda.md | 4 --- .../strict-inequality-real-numbers.lagda.md | 2 +- 12 files changed, 67 insertions(+), 56 deletions(-) create mode 100644 src/real-numbers/similarity-positive-real-numbers.lagda.md diff --git a/src/real-numbers/absolute-value-closed-intervals-real-numbers.lagda.md b/src/real-numbers/absolute-value-closed-intervals-real-numbers.lagda.md index f040689b7c..634f6c9034 100644 --- a/src/real-numbers/absolute-value-closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/absolute-value-closed-intervals-real-numbers.lagda.md @@ -49,8 +49,6 @@ abstract leq-ℝ (abs-ℝ z) (max-abs-closed-interval-ℝ [x,y]) leq-max-abs-is-in-closed-interval-ℝ ((x , y) , x≤y) z (x≤z , z≤y) = leq-abs-leq-leq-neg-ℝ - ( z) - ( max-ℝ (neg-ℝ x) y) ( transitive-leq-ℝ _ _ _ (leq-right-max-ℝ _ _) z≤y) ( transitive-leq-ℝ _ _ _ (leq-left-max-ℝ _ _) (neg-leq-ℝ x≤z)) ``` diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md index d31b66d8b8..8d3c38266f 100644 --- a/src/real-numbers/absolute-value-real-numbers.lagda.md +++ b/src/real-numbers/absolute-value-real-numbers.lagda.md @@ -66,7 +66,7 @@ opaque ### The absolute value of zero is zero ```agda -opaque +abstract opaque unfolding abs-ℝ abs-zero-ℝ : abs-ℝ zero-ℝ = zero-ℝ @@ -76,7 +76,7 @@ opaque ### The absolute value preserves similarity ```agda -opaque +abstract opaque unfolding abs-ℝ preserves-sim-abs-ℝ : @@ -89,7 +89,7 @@ opaque ### The absolute value of a real number is nonnegative ```agda -opaque +abstract opaque unfolding abs-ℝ leq-ℝ max-ℝ neg-ℚ neg-ℝ real-ℚ is-nonnegative-abs-ℝ : {l : Level} → (x : ℝ l) → is-nonnegative-ℝ (abs-ℝ x) @@ -210,10 +210,10 @@ module _ ```agda module _ - {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) + {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} where - opaque + abstract opaque unfolding abs-ℝ leq-abs-leq-leq-neg-ℝ : leq-ℝ x y → leq-ℝ (neg-ℝ x) y → leq-ℝ (abs-ℝ x) y @@ -231,8 +231,6 @@ module _ triangle-inequality-abs-ℝ : leq-ℝ (abs-ℝ (x +ℝ y)) (abs-ℝ x +ℝ abs-ℝ y) triangle-inequality-abs-ℝ = leq-abs-leq-leq-neg-ℝ - ( x +ℝ y) - ( abs-ℝ x +ℝ abs-ℝ y) ( preserves-leq-add-ℝ (leq-abs-ℝ x) (leq-abs-ℝ y)) ( inv-tr ( λ z → leq-ℝ z (abs-ℝ x +ℝ abs-ℝ y)) @@ -259,8 +257,6 @@ module _ ( abs-ℝ x) ( abs-ℝ y) ( leq-abs-leq-leq-neg-ℝ - ( x) - ( abs-ℝ y +ℝ real-ℚ⁺ d) ( transitive-leq-ℝ ( x) ( y +ℝ real-ℚ⁺ d) @@ -286,8 +282,6 @@ module _ ( x) ( right-leq-real-bound-neighborhood-ℝ d x y I)))) ( leq-abs-leq-leq-neg-ℝ - ( y) - ( abs-ℝ x +ℝ real-ℚ⁺ d) ( transitive-leq-ℝ ( y) ( x +ℝ real-ℚ⁺ d) diff --git a/src/real-numbers/distance-real-numbers.lagda.md b/src/real-numbers/distance-real-numbers.lagda.md index df3a005ee3..1f779167f0 100644 --- a/src/real-numbers/distance-real-numbers.lagda.md +++ b/src/real-numbers/distance-real-numbers.lagda.md @@ -83,11 +83,13 @@ nonnegative-dist-ℝ x y = (dist-ℝ x y , is-nonnegative-dist-ℝ x y) ### Relationship to the metric space of real numbers -Two real numbers `x` and `y` are in an `ε`-neighborhood of each other if and -only if their distance is at most `ε`. +Two real numbers `x` and `y` are in an `ε`-neighborhood of each other in the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md) +[if and only if](foundation.logical-equivalences.md) their distance is +[at most](real-numbers.inequality-real-numbers.md) `ε`. ```agda -opaque +abstract opaque unfolding leq-ℝ neighborhood-ℝ diff-bound-neighborhood-ℝ : @@ -125,8 +127,6 @@ abstract dist-ℝ x y ≤-ℝ real-ℚ⁺ d leq-dist-neighborhood-ℝ d⁺@(d , _) x y H = leq-abs-leq-leq-neg-ℝ - ( x -ℝ y) - ( real-ℚ d) ( diff-bound-neighborhood-ℝ d⁺ x y H) ( inv-tr ( λ z → leq-ℝ z (real-ℚ d)) @@ -236,8 +236,6 @@ abstract dist-ℝ x y ≤-ℝ z leq-dist-leq-diff-ℝ x y z x-y≤z y-x≤z = leq-abs-leq-leq-neg-ℝ - ( _) - ( z) ( x-y≤z) ( inv-tr (λ w → leq-ℝ w z) (distributive-neg-diff-ℝ _ _) y-x≤z) @@ -259,7 +257,7 @@ abstract preserves-dist-left-add-ℝ : {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) → sim-ℝ - ( dist-ℝ (add-ℝ x y) (add-ℝ x z)) + ( dist-ℝ (x +ℝ y) (x +ℝ z)) ( dist-ℝ y z) preserves-dist-left-add-ℝ x y z = similarity-reasoning-ℝ @@ -280,7 +278,7 @@ abstract preserves-dist-right-add-ℝ : {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) → sim-ℝ - ( dist-ℝ (add-ℝ x z) (add-ℝ y z)) + ( dist-ℝ (x +ℝ z) (y +ℝ z)) ( dist-ℝ x y) preserves-dist-right-add-ℝ z x y = similarity-reasoning-ℝ diff --git a/src/real-numbers/inequalities-addition-real-numbers.lagda.md b/src/real-numbers/inequalities-addition-real-numbers.lagda.md index 654f922bc1..aa5f3ad62e 100644 --- a/src/real-numbers/inequalities-addition-real-numbers.lagda.md +++ b/src/real-numbers/inequalities-addition-real-numbers.lagda.md @@ -73,10 +73,6 @@ module _ reflects-leq-right-add-ℝ : leq-ℝ (x +ℝ z) (y +ℝ z) → leq-ℝ x y reflects-leq-right-add-ℝ x+z≤y+z = preserves-leq-sim-ℝ - ( (x +ℝ z) -ℝ z) - ( x) - ( (y +ℝ z) -ℝ z) - ( y) ( cancel-right-add-diff-ℝ x z) ( cancel-right-add-diff-ℝ y z) ( preserves-leq-right-add-ℝ (neg-ℝ z) (x +ℝ z) (y +ℝ z) x+z≤y+z) diff --git a/src/real-numbers/inequality-real-numbers.lagda.md b/src/real-numbers/inequality-real-numbers.lagda.md index d9b18435f1..d0a0cd049c 100644 --- a/src/real-numbers/inequality-real-numbers.lagda.md +++ b/src/real-numbers/inequality-real-numbers.lagda.md @@ -337,7 +337,7 @@ module _ module _ {l1 l2 l3 l4 : Level} - (x1 : ℝ l1) (x2 : ℝ l2) (y1 : ℝ l3) (y2 : ℝ l4) + {x1 : ℝ l1} {x2 : ℝ l2} {y1 : ℝ l3} {y2 : ℝ l4} (x1~x2 : sim-ℝ x1 x2) (y1~y2 : sim-ℝ y1 y2) where 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 5afe6b7b56..7a64835572 100644 --- a/src/real-numbers/metric-space-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-space-of-real-numbers.lagda.md @@ -355,10 +355,6 @@ module _ ( x') ( y') ( preserves-leq-sim-ℝ - ( x) - ( x') - ( y +ℝ real-ℚ⁺ d) - ( y' +ℝ real-ℚ⁺ d) ( x~x') ( preserves-sim-right-add-ℝ ( real-ℚ⁺ d) @@ -367,10 +363,6 @@ module _ ( y~y')) ( left-leq-real-bound-neighborhood-ℝ d x y H)) ( preserves-leq-sim-ℝ - ( y) - ( y') - ( x +ℝ real-ℚ⁺ d) - ( x' +ℝ real-ℚ⁺ d) ( y~y') ( preserves-sim-right-add-ℝ ( real-ℚ⁺ d) diff --git a/src/real-numbers/multiplication-positive-real-numbers.lagda.md b/src/real-numbers/multiplication-positive-real-numbers.lagda.md index 0c7aeb5307..ab63080b99 100644 --- a/src/real-numbers/multiplication-positive-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-positive-real-numbers.lagda.md @@ -123,7 +123,7 @@ abstract {l1 l2 l3 : Level} (x : ℝ⁺ l1) (y : ℝ l2) (z : ℝ l3) → le-ℝ (real-ℝ⁺ x *ℝ y) (real-ℝ⁺ x *ℝ z) → le-ℝ y z reflects-le-left-mul-ℝ⁺ x y z xy @@ -102,8 +102,12 @@ upper-cut-ℝ⁰⁺ (x , _) = upper-cut-ℝ x is-in-upper-cut-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → ℚ → UU l is-in-upper-cut-ℝ⁰⁺ (x , _) = is-in-upper-cut-ℝ x +is-inhabited-upper-cut-ℝ⁰⁺ : + {l : Level} (x : ℝ⁰⁺ l) → is-inhabited-subtype (upper-cut-ℝ⁰⁺ x) +is-inhabited-upper-cut-ℝ⁰⁺ (x , _) = is-inhabited-upper-cut-ℝ x + is-rounded-upper-cut-ℝ⁰⁺ : - {l : Level} → (x : ℝ⁰⁺ l) (r : ℚ) → + {l : Level} (x : ℝ⁰⁺ l) (r : ℚ) → (is-in-upper-cut-ℝ⁰⁺ x r ↔ exists ℚ (λ q → le-ℚ-Prop q r ∧ upper-cut-ℝ⁰⁺ x q)) is-rounded-upper-cut-ℝ⁰⁺ (x , _) = is-rounded-upper-cut-ℝ x ``` @@ -163,8 +167,8 @@ abstract ( 0≤x) ( le-real-is-in-upper-cut-ℚ x xImports + +```agda +open import foundation.universe-levels +open import foundation.propositions +open import real-numbers.positive-real-numbers +open import real-numbers.similarity-real-numbers +open import foundation.dependent-pair-types +``` + + + +## Idea + +Two [positive](real-numbers.positive-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are +{{#concept "similar" Disambiguation="positive real numbers" Agda=sim-ℝ⁺}} if +they are [similar](real-numbers.similarity-real-numbers.md) as real numbers. + +## Definition + +```agda +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 +``` diff --git a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md index 978356cd75..e28ec7bda1 100644 --- a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md @@ -131,10 +131,6 @@ module _ reflects-le-right-add-ℝ : le-ℝ (x +ℝ z) (y +ℝ z) → le-ℝ x y reflects-le-right-add-ℝ x+z Date: Fri, 7 Nov 2025 15:07:38 -0800 Subject: [PATCH 03/21] Progress --- .../powers-positive-rational-numbers.lagda.md | 4 ++-- ...ic-spaces-are-uniformly-continuous.lagda.md | 18 ++++++++++-------- src/real-numbers.lagda.md | 1 + .../nonnegative-real-numbers.lagda.md | 4 ++-- .../similarity-positive-real-numbers.lagda.md | 5 +++-- 5 files changed, 18 insertions(+), 14 deletions(-) diff --git a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md index 1f3932919c..08a63343eb 100644 --- a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md @@ -197,8 +197,8 @@ abstract Σ ℕ (λ n → le-ℚ b (rational-ℚ⁺ (power-ℚ⁺ n q))) bound-unbounded-power-greater-than-one-ℚ⁺ q⁺@(q , _) b 1Imports ```agda -open import foundation.universe-levels +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 -open import foundation.dependent-pair-types ``` From 007d5876181591352e3536ca324d4fc69dcb13e1 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 7 Nov 2025 15:59:13 -0800 Subject: [PATCH 04/21] Progress --- ...ddition-positive-rational-numbers.lagda.md | 8 +- ...ive-and-negative-rational-numbers.lagda.md | 8 +- ...closed-intervals-rational-numbers.lagda.md | 44 ++--- .../negative-rational-numbers.lagda.md | 18 +- ...ive-and-negative-rational-numbers.lagda.md | 12 +- .../positive-rational-numbers.lagda.md | 9 +- ...wers-nonnegative-rational-numbers.lagda.md | 2 +- .../squares-rational-numbers.lagda.md | 2 +- ...quality-positive-rational-numbers.lagda.md | 6 +- ...trict-inequality-rational-numbers.lagda.md | 11 +- .../located-metric-spaces.lagda.md | 5 +- src/real-numbers.lagda.md | 1 + .../addition-real-numbers.lagda.md | 104 +++-------- .../binary-maximum-real-numbers.lagda.md | 161 ++--------------- ...lication-nonnegative-real-numbers.lagda.md | 3 +- ...tiplication-positive-real-numbers.lagda.md | 6 +- .../multiplication-real-numbers.lagda.md | 32 ++-- ...ve-inverses-positive-real-numbers.lagda.md | 17 +- .../negation-real-numbers.lagda.md | 13 -- .../nonnegative-real-numbers.lagda.md | 7 - ...ional-lower-dedekind-real-numbers.lagda.md | 2 +- ...ional-upper-dedekind-real-numbers.lagda.md | 2 +- ...-from-lower-dedekind-real-numbers.lagda.md | 8 +- ...-from-upper-dedekind-real-numbers.lagda.md | 11 +- ...short-binary-maximum-real-numbers.lagda.md | 166 ++++++++++++++++++ ...re-roots-nonnegative-real-numbers.lagda.md | 8 +- .../squares-real-numbers.lagda.md | 2 - .../strict-inequality-real-numbers.lagda.md | 5 +- 28 files changed, 303 insertions(+), 370 deletions(-) create mode 100644 src/real-numbers/short-binary-maximum-real-numbers.lagda.md 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 7e1cf13e5b..78b872ffe9 100644 --- a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md @@ -334,16 +334,16 @@ module _ ((d : ℚ⁺) → leq-ℚ x (y +ℚ (rational-ℚ⁺ d))) → leq-ℚ x y leq-leq-add-positive-ℚ H = rec-coproduct - ( λ I → + ( λ yImports ```agda -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.action-on-identifications-functions -open import foundation.cartesian-product-types -open import foundation.conjunction -open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.disjoint-subtypes open import foundation.disjunction -open import foundation.empty-types -open import foundation.existential-quantification open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences -open import foundation.negation -open import foundation.propositional-truncations -open import foundation.propositions open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import logic.functoriality-existential-quantification - open import real-numbers.dedekind-real-numbers open import real-numbers.lower-dedekind-real-numbers open import real-numbers.negation-lower-upper-dedekind-real-numbers -open import real-numbers.rational-lower-dedekind-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.rational-upper-dedekind-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.upper-dedekind-real-numbers ``` diff --git a/src/real-numbers/nonnegative-real-numbers.lagda.md b/src/real-numbers/nonnegative-real-numbers.lagda.md index c2f3447dd1..fcb7e126e0 100644 --- a/src/real-numbers/nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/nonnegative-real-numbers.lagda.md @@ -9,8 +9,6 @@ module real-numbers.nonnegative-real-numbers where
Imports ```agda -open import elementary-number-theory.addition-nonnegative-rational-numbers -open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers @@ -20,17 +18,13 @@ open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.conjunction -open import foundation.coproduct-types open import foundation.dependent-pair-types -open import foundation.empty-types open import foundation.existential-quantification -open import foundation.function-types open import foundation.functoriality-propositional-truncation open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.logical-equivalences open import foundation.negation -open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes @@ -45,7 +39,6 @@ open import real-numbers.difference-real-numbers open import real-numbers.inequalities-addition-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.similarity-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md index 5176279b29..3dbae48f3b 100644 --- a/src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md @@ -50,7 +50,7 @@ module _ pr1 (is-rounded-cut-lower-real-ℚ p) pImports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.binary-transport +open import foundation.dependent-pair-types +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 order-theory.least-upper-bounds-large-posets + +open import real-numbers.addition-real-numbers +open import real-numbers.binary-maximum-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.inequalities-addition-real-numbers +open import real-numbers.inequality-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.strict-inequality-real-numbers +``` + +
+ +## Idea + +For any `a : ℝ`, the +[binary maximum](real-numbers.binary-maximum-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). +Moreover, the map `x ↦ max-ℝ x` is a short function from `ℝ` into the +[metric space of short functions](metric-spaces.metric-space-of-short-functions-metric-spaces.md) +of `ℝ`. + +## Proof + +### The binary maximum preserves lower neighborhoods + +```agda +module _ + {l1 l2 l3 : Level} (d : ℚ⁺) + (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) + where + + abstract + preserves-lower-neighborhood-leq-left-max-ℝ : + leq-ℝ y (z +ℝ real-ℚ⁺ d) → + leq-ℝ + ( max-ℝ x y) + ( (max-ℝ x z) +ℝ real-ℚ⁺ d) + preserves-lower-neighborhood-leq-left-max-ℝ z≤y+d = + leq-is-least-binary-upper-bound-Large-Poset + ( ℝ-Large-Poset) + ( x) + ( y) + ( is-least-binary-upper-bound-max-ℝ x y) + ( (max-ℝ x z) +ℝ real-ℚ⁺ d) + ( ( transitive-leq-ℝ + ( x) + ( max-ℝ x z) + ( max-ℝ x z +ℝ real-ℚ⁺ d) + ( leq-le-ℝ + ( le-left-add-real-ℝ⁺ + ( max-ℝ x z) + ( positive-real-ℚ⁺ d))) + ( leq-left-max-ℝ x z)) , + ( transitive-leq-ℝ + ( y) + ( z +ℝ real-ℚ⁺ d) + ( max-ℝ x z +ℝ real-ℚ⁺ d) + ( preserves-leq-right-add-ℝ + ( real-ℚ⁺ d) + ( z) + ( max-ℝ x z) + ( leq-right-max-ℝ x z)) + ( z≤y+d))) + + preserves-lower-neighborhood-leq-right-max-ℝ : + leq-ℝ y (z +ℝ real-ℚ⁺ d) → + leq-ℝ + ( max-ℝ y x) + ( (max-ℝ z x) +ℝ real-ℚ⁺ d) + preserves-lower-neighborhood-leq-right-max-ℝ z≤y+d = + binary-tr + ( λ u v → leq-ℝ u (v +ℝ real-ℚ⁺ d)) + ( commutative-max-ℝ x y) + ( commutative-max-ℝ x z) + ( preserves-lower-neighborhood-leq-left-max-ℝ z≤y+d) +``` + +### The maximum with a real number is a short function `ℝ → ℝ` + +```agda +module _ + {l1 l2 : Level} (x : ℝ l1) + where + + abstract + is-short-function-left-max-ℝ : + is-short-function-Metric-Space + ( metric-space-ℝ l2) + ( metric-space-ℝ (l1 ⊔ l2)) + ( max-ℝ x) + is-short-function-left-max-ℝ d y z Nyz = + neighborhood-real-bound-each-leq-ℝ + ( d) + ( max-ℝ x y) + ( max-ℝ x z) + ( preserves-lower-neighborhood-leq-left-max-ℝ d x y z + ( left-leq-real-bound-neighborhood-ℝ d y z Nyz)) + ( preserves-lower-neighborhood-leq-left-max-ℝ d x z y + ( right-leq-real-bound-neighborhood-ℝ d y z Nyz)) + + short-left-max-ℝ : + short-function-Metric-Space + ( metric-space-ℝ l2) + ( metric-space-ℝ (l1 ⊔ l2)) + short-left-max-ℝ = + (max-ℝ x , is-short-function-left-max-ℝ) +``` + +### The binary maximum is a short function from `ℝ` to the metric space of short functions `ℝ → ℝ` + +```agda +module _ + {l1 l2 : Level} + where + + abstract + is-short-function-short-left-max-ℝ : + is-short-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-of-short-functions-Metric-Space + ( metric-space-ℝ l2) + ( metric-space-ℝ (l1 ⊔ l2))) + ( short-left-max-ℝ) + is-short-function-short-left-max-ℝ d x y Nxy z = + neighborhood-real-bound-each-leq-ℝ + ( d) + ( max-ℝ x z) + ( max-ℝ y z) + ( preserves-lower-neighborhood-leq-right-max-ℝ d z x y + ( left-leq-real-bound-neighborhood-ℝ d x y Nxy)) + ( preserves-lower-neighborhood-leq-right-max-ℝ d z y x + ( right-leq-real-bound-neighborhood-ℝ d x y Nxy)) + + short-max-ℝ : + short-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-of-short-functions-Metric-Space + ( metric-space-ℝ l2) + ( metric-space-ℝ (l1 ⊔ l2))) + short-max-ℝ = + (short-left-max-ℝ , is-short-function-short-left-max-ℝ) +``` diff --git a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md index 154237168d..dce82321de 100644 --- a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md @@ -164,7 +164,6 @@ module _ is-pos-p = is-positive-le-ℚ⁺ ( q *ℚ q , is-positive-mul-ℚ is-pos-q is-pos-q) - ( p) ( q² Date: Fri, 7 Nov 2025 17:01:54 -0800 Subject: [PATCH 05/21] Progress --- .../metrics-of-metric-spaces.lagda.md | 1 + .../absolute-value-real-numbers.lagda.md | 2 +- .../addition-real-numbers.lagda.md | 4 +- ...thmetically-located-dedekind-cuts.lagda.md | 6 +- ...ompleteness-dedekind-real-numbers.lagda.md | 8 -- .../dedekind-real-numbers.lagda.md | 9 +- .../distance-real-numbers.lagda.md | 2 +- ...d-rational-intervals-real-numbers.lagda.md | 13 +- ...nequalities-addition-real-numbers.lagda.md | 2 +- ...ality-lower-dedekind-real-numbers.lagda.md | 2 - .../inequality-real-numbers.lagda.md | 14 +- ...nuity-multiplication-real-numbers.lagda.md | 2 - .../metric-space-of-real-numbers.lagda.md | 5 +- ...tiplication-negative-real-numbers.lagda.md | 12 +- ...lication-nonnegative-real-numbers.lagda.md | 14 +- ...tiplication-positive-real-numbers.lagda.md | 32 ++--- .../multiplication-real-numbers.lagda.md | 24 ++-- ...ve-inverses-positive-real-numbers.lagda.md | 31 ++-- ...lower-upper-dedekind-real-numbers.lagda.md | 21 ++- .../negation-real-numbers.lagda.md | 4 +- .../positive-real-numbers.lagda.md | 8 +- .../rational-real-numbers.lagda.md | 2 +- .../similarity-real-numbers.lagda.md | 14 +- ...re-roots-nonnegative-real-numbers.lagda.md | 34 ++--- .../squares-real-numbers.lagda.md | 10 +- ...nequalities-addition-real-numbers.lagda.md | 33 ++++- .../strict-inequality-real-numbers.lagda.md | 135 +++++------------- 27 files changed, 180 insertions(+), 264 deletions(-) diff --git a/src/metric-spaces/metrics-of-metric-spaces.lagda.md b/src/metric-spaces/metrics-of-metric-spaces.lagda.md index 7a8cea0f77..d113ff5bac 100644 --- a/src/metric-spaces/metrics-of-metric-spaces.lagda.md +++ b/src/metric-spaces/metrics-of-metric-spaces.lagda.md @@ -28,6 +28,7 @@ open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.saturation-inequality-nonnegative-real-numbers open import real-numbers.similarity-nonnegative-real-numbers +open import real-numbers.strict-inequalities-addition-real-numbers open import real-numbers.strict-inequality-nonnegative-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md index 8d3c38266f..0ebbeb29d4 100644 --- a/src/real-numbers/absolute-value-real-numbers.lagda.md +++ b/src/real-numbers/absolute-value-real-numbers.lagda.md @@ -107,7 +107,7 @@ nonnegative-abs-ℝ x = (abs-ℝ x , is-nonnegative-abs-ℝ x) ### The absolute value of the negation of a real number is its absolute value ```agda -opaque +abstract opaque unfolding abs-ℝ abs-neg-ℝ : {l : Level} → (x : ℝ l) → abs-ℝ (neg-ℝ x) = abs-ℝ x diff --git a/src/real-numbers/addition-real-numbers.lagda.md b/src/real-numbers/addition-real-numbers.lagda.md index fa74b6a4c7..fef1ddfc68 100644 --- a/src/real-numbers/addition-real-numbers.lagda.md +++ b/src/real-numbers/addition-real-numbers.lagda.md @@ -88,8 +88,8 @@ module _ { qx} { py} { qy} - ( le-lower-upper-cut-ℝ x px qx px @@ -62,7 +50,7 @@ The {{#concept "standard ordering" Disambiguation="real numbers" Agda=leq-ℝ}} the [real numbers](real-numbers.dedekind-real-numbers.md) is defined as the [lower cut](real-numbers.lower-dedekind-real-numbers.md) of one being a [subset](foundation-core.subtypes.md) of the lower cut of the other. I.e., -`x ≤ y` if `lower-cut x ⊆ lower-cut y `. This is the definition used in +`x ≤ y` if `lower-cut-ℝ x ⊆ lower-cut-ℝ y `. This is the definition used in {{#cite UF13}}, section 11.2.1. Inequality of the real numbers is equivalently described by the _upper_ cut of diff --git a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md index 7b3d8f8c66..ed960956fe 100644 --- a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md +++ b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md @@ -258,8 +258,6 @@ module _ by preserves-leq-right-mul-ℝ⁰⁺ ( nonnegative-real-ℚ⁺ ε) - ( my +ℝ mx) - ( real-ℚ q) ( leq-le-ℝ (le-real-is-in-upper-cut-ℚ (my +ℝ mx) my+mxImports ```agda -open import elementary-number-theory.addition-rational-numbers -open import elementary-number-theory.additive-group-of-rational-numbers -open import elementary-number-theory.difference-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.action-on-identifications-functions -open import foundation.binary-transport -open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.coproduct-types open import foundation.dependent-pair-types @@ -28,26 +21,19 @@ open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-disjunction -open import foundation.identity-types open import foundation.large-binary-relations open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions -open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.universe-levels -open import group-theory.abelian-groups - open import logic.functoriality-existential-quantification -open import real-numbers.addition-real-numbers -open import real-numbers.arithmetically-located-dedekind-cuts 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.negation-real-numbers open import real-numbers.rational-real-numbers @@ -81,34 +67,28 @@ le-prop-ℝ x y = (le-ℝ x y , is-prop-le-ℝ x y) ### Strict inequality on the reals implies inequality ```agda -opaque +abstract opaque unfolding le-ℝ leq-ℝ leq-le-ℝ : {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → le-ℝ x y → leq-ℝ x y leq-le-ℝ {x = x} {y = y} x Date: Fri, 7 Nov 2025 17:07:50 -0800 Subject: [PATCH 06/21] Mark more things abstract opaque --- .../binary-minimum-real-numbers.lagda.md | 4 ++-- ...ompleteness-dedekind-real-numbers.lagda.md | 4 ++-- .../closed-intervals-real-numbers.lagda.md | 2 +- .../inequality-real-numbers.lagda.md | 22 +++++++++---------- 4 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/real-numbers/binary-minimum-real-numbers.lagda.md b/src/real-numbers/binary-minimum-real-numbers.lagda.md index 121bf5d42b..b0ae4c0640 100644 --- a/src/real-numbers/binary-minimum-real-numbers.lagda.md +++ b/src/real-numbers/binary-minimum-real-numbers.lagda.md @@ -66,7 +66,7 @@ module _ (x : ℝ l1) (y : ℝ l2) where - opaque + abstract opaque unfolding leq-ℝ min-ℝ is-greatest-binary-lower-bound-min-ℝ : @@ -155,7 +155,7 @@ module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where - opaque + abstract opaque unfolding min-ℝ approximate-above-min-ℝ : diff --git a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md index 57f47ac4dd..ab073ba3c2 100644 --- a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md @@ -299,7 +299,7 @@ module _ is-inhabited-upper-cut-lim-cauchy-approximation-ℝ , is-rounded-upper-cut-lim-cauchy-approximation-ℝ - opaque + abstract opaque unfolding neighborhood-ℝ is-disjoint-cut-lim-cauchy-approximation-ℝ : @@ -411,7 +411,7 @@ module _ {l : Level} (x : cauchy-approximation-ℝ l) where - opaque + abstract opaque unfolding le-ℝ lim-cauchy-approximation-ℝ is-limit-lim-cauchy-approximation-ℝ : diff --git a/src/real-numbers/closed-intervals-real-numbers.lagda.md b/src/real-numbers/closed-intervals-real-numbers.lagda.md index 846087aa48..d8460f5bdc 100644 --- a/src/real-numbers/closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/closed-intervals-real-numbers.lagda.md @@ -90,7 +90,7 @@ unit-closed-interval-ℝ = ### Closed intervals in the real numbers are closed in the metric space of real numbers ```agda -opaque +abstract opaque unfolding leq-ℝ neighborhood-ℝ is-closed-subset-closed-interval-ℝ : diff --git a/src/real-numbers/inequality-real-numbers.lagda.md b/src/real-numbers/inequality-real-numbers.lagda.md index 89c0fbbb57..4ece5ae59a 100644 --- a/src/real-numbers/inequality-real-numbers.lagda.md +++ b/src/real-numbers/inequality-real-numbers.lagda.md @@ -127,7 +127,7 @@ module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where - opaque + abstract opaque unfolding leq-ℝ leq-ℝ' leq'-leq-ℝ : leq-ℝ x y → leq-ℝ' x y @@ -175,7 +175,7 @@ module _ ### Inequality on the real numbers is reflexive ```agda -opaque +abstract opaque unfolding leq-ℝ refl-leq-ℝ : {l : Level} (x : ℝ l) → leq-ℝ x x @@ -184,7 +184,7 @@ opaque leq-eq-ℝ : {l : Level} {x y : ℝ l} → x = y → leq-ℝ x y leq-eq-ℝ {x = x} refl = refl-leq-ℝ x -opaque +abstract opaque unfolding leq-ℝ sim-ℝ leq-sim-ℝ : {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → sim-ℝ x y → leq-ℝ x y @@ -194,7 +194,7 @@ opaque ### Inequality on the real numbers is antisymmetric ```agda -opaque +abstract opaque unfolding leq-ℝ sim-ℝ sim-antisymmetric-leq-ℝ : @@ -215,7 +215,7 @@ module _ (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where - opaque + abstract opaque unfolding leq-ℝ transitive-leq-ℝ : leq-ℝ y z → leq-ℝ x y → leq-ℝ x z @@ -244,7 +244,7 @@ antisymmetric-leq-Large-Poset ℝ-Large-Poset = antisymmetric-leq-ℝ ### Similarity in the large poset of real numbers is equivalent to similarity ```agda -opaque +abstract opaque unfolding leq-ℝ sim-ℝ sim-sim-leq-ℝ : @@ -280,7 +280,7 @@ module _ {x y : ℚ} where - opaque + abstract opaque unfolding leq-ℝ real-ℚ preserves-leq-real-ℚ : leq-ℚ x y → leq-ℝ (real-ℚ x) (real-ℚ y) @@ -300,7 +300,7 @@ module _ {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} where - opaque + abstract opaque unfolding leq-ℝ leq-ℝ' neg-ℝ neg-leq-ℝ : leq-ℝ x y → leq-ℝ (neg-ℝ y) (neg-ℝ x) @@ -314,7 +314,7 @@ module _ {l1 l2 l3 : Level} {z : ℝ l1} {x : ℝ l2} {y : ℝ l3} (x~y : sim-ℝ x y) where - opaque + abstract opaque unfolding leq-ℝ sim-ℝ preserves-leq-left-sim-ℝ : leq-ℝ x z → leq-ℝ y z @@ -343,7 +343,7 @@ module _ {l : Level} (x : ℝ l) (q : ℚ) where - opaque + abstract opaque unfolding leq-ℝ leq-ℝ' real-ℚ not-in-lower-cut-leq-ℝ : leq-ℝ x (real-ℚ q) → ¬ (is-in-lower-cut-ℝ x q) @@ -376,7 +376,7 @@ module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where - opaque + abstract opaque unfolding leq-ℝ' leq-leq-rational-ℝ : From 04ccb85e348ae65c7afe3dd091e99585f0a20d4a Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 7 Nov 2025 17:09:00 -0800 Subject: [PATCH 07/21] Fix indent --- src/real-numbers/addition-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/addition-real-numbers.lagda.md b/src/real-numbers/addition-real-numbers.lagda.md index fef1ddfc68..356d51654f 100644 --- a/src/real-numbers/addition-real-numbers.lagda.md +++ b/src/real-numbers/addition-real-numbers.lagda.md @@ -97,7 +97,7 @@ module _ let open do-syntax-trunc-Prop - (∃ + ( ∃ ( ℚ × ℚ) ( close-bounds-lower-upper-ℝ ( lower-real-add-ℝ) From 1d65b0a47540f785cc9142871450b6018706fbcb Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 7 Nov 2025 17:13:56 -0800 Subject: [PATCH 08/21] Fix title --- src/real-numbers/short-binary-maximum-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/short-binary-maximum-real-numbers.lagda.md b/src/real-numbers/short-binary-maximum-real-numbers.lagda.md index 2ac42192c9..5dd32621e1 100644 --- a/src/real-numbers/short-binary-maximum-real-numbers.lagda.md +++ b/src/real-numbers/short-binary-maximum-real-numbers.lagda.md @@ -1,4 +1,4 @@ -## The binary maximum of real numbers is a short function +# The binary maximum of real numbers is a short function ```agda {-# OPTIONS --lossy-unification #-} From 84dec2a5fc910c14f47edcb4457754f5cbe8d797 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 7 Nov 2025 17:14:54 -0800 Subject: [PATCH 09/21] Fix --- src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index f70d4ca8b4..1592876b21 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -298,8 +298,6 @@ module _ ( p Date: Sat, 8 Nov 2025 11:53:39 -0800 Subject: [PATCH 10/21] Update src/real-numbers/dedekind-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- src/real-numbers/dedekind-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 0c1531e91f..d846a3556d 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -312,7 +312,7 @@ module _ ( lower-cut-ℝ x p) ( upper-cut-ℝ x q) ( pr2 I) - ( is-located-lower-upper-cut-ℝ x ( pr1 I))) + ( is-located-lower-upper-cut-ℝ x (pr1 I))) subset-lower-complement-upper-cut-lower-cut-ℝ : lower-cut-ℝ x ⊆ lower-complement-upper-cut-ℝ x From d9aeb7fda4ea62f8502e4183945b386f770f1137 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 11:55:14 -0800 Subject: [PATCH 11/21] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- .../strict-inequalities-addition-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md index 6db92caf63..1c8789dd67 100644 --- a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md @@ -293,7 +293,7 @@ module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) (p : ℚ) where - opaque + abstract opaque unfolding add-ℝ le-split-add-rational-ℝ : From defa2134d99b91f3aaf396f1200f6e6c47458ecd Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 11:55:32 -0800 Subject: [PATCH 12/21] Update src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- .../strict-inequalities-addition-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md index 1c8789dd67..9403114e3a 100644 --- a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md @@ -59,7 +59,7 @@ module _ {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) where - opaque + abstract opaque unfolding add-ℝ le-ℝ preserves-le-right-add-ℝ : le-ℝ x y → le-ℝ (x +ℝ z) (y +ℝ z) From fa31c521b7092f0e46eea6d3cf8904418d952271 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 11:55:52 -0800 Subject: [PATCH 13/21] Update src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- .../strict-inequalities-addition-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md index 9403114e3a..24417dab87 100644 --- a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md @@ -44,7 +44,7 @@ open import real-numbers.strict-inequality-real-numbers ## Idea -This file describes lemmas about +On this page we describe lemmas about [strict inequalities](real-numbers.strict-inequality-real-numbers.md) of [real numbers](real-numbers.dedekind-real-numbers.md) related to [addition](real-numbers.addition-real-numbers.md) and From 45757e8f51bf8fccacfd913a0fed7853b7eb9726 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 11:57:09 -0800 Subject: [PATCH 14/21] Update src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- .../saturation-inequality-nonnegative-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md b/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md index 037e54c2f2..69f3a5fb11 100644 --- a/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md @@ -36,7 +36,7 @@ Despite being a property of [inequality of nonnegative real numbers](real-numbers.inequality-nonnegative-real-numbers.md), this is much easier to prove via [strict inequality](real-numbers.strict-inequality-nonnegative-real-numbers.md), -so it is moved to its own file to prevent circular dependency. +so this page is dedicated to just this property to prevent circular dependency. ## Definition From 70cef9b710f6564e4559bff99dae0a07f25883ca Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 11:59:33 -0800 Subject: [PATCH 15/21] Rename files --- ...trics-of-metric-spaces-are-uniformly-continuous.lagda.md | 2 +- src/metric-spaces/metrics-of-metric-spaces.lagda.md | 2 +- src/real-numbers.lagda.md | 6 +++--- src/real-numbers/absolute-value-real-numbers.lagda.md | 2 +- src/real-numbers/addition-nonnegative-real-numbers.lagda.md | 4 ++-- src/real-numbers/binary-maximum-real-numbers.lagda.md | 2 +- .../cauchy-completeness-dedekind-real-numbers.lagda.md | 2 +- src/real-numbers/distance-real-numbers.lagda.md | 2 +- ...ualities-addition-and-subtraction-real-numbers.lagda.md} | 2 +- src/real-numbers/infima-families-real-numbers.lagda.md | 2 +- .../inhabited-totally-bounded-subsets-real-numbers.lagda.md | 4 ++-- src/real-numbers/isometry-addition-real-numbers.lagda.md | 2 +- src/real-numbers/isometry-negation-real-numbers.lagda.md | 2 +- ...ipschitz-continuity-multiplication-real-numbers.lagda.md | 2 +- .../maximum-finite-families-real-numbers.lagda.md | 2 +- src/real-numbers/metric-space-of-real-numbers.lagda.md | 4 ++-- src/real-numbers/nonnegative-real-numbers.lagda.md | 2 +- src/real-numbers/positive-real-numbers.lagda.md | 2 +- .../saturation-inequality-real-numbers.lagda.md | 2 +- ... => short-function-binary-maximum-real-numbers.lagda.md} | 4 ++-- ...ualities-addition-and-subtraction-real-numbers.lagda.md} | 2 +- src/real-numbers/suprema-families-real-numbers.lagda.md | 2 +- ...addition-subtraction-cuts-dedekind-real-numbers.lagda.md | 2 +- 23 files changed, 29 insertions(+), 29 deletions(-) rename src/real-numbers/{inequalities-addition-real-numbers.lagda.md => inequalities-addition-and-subtraction-real-numbers.lagda.md} (98%) rename src/real-numbers/{short-binary-maximum-real-numbers.lagda.md => short-function-binary-maximum-real-numbers.lagda.md} (97%) rename src/real-numbers/{strict-inequalities-addition-real-numbers.lagda.md => strict-inequalities-addition-and-subtraction-real-numbers.lagda.md} (99%) diff --git a/src/metric-spaces/metrics-of-metric-spaces-are-uniformly-continuous.lagda.md b/src/metric-spaces/metrics-of-metric-spaces-are-uniformly-continuous.lagda.md index c33453db28..0eed19b179 100644 --- a/src/metric-spaces/metrics-of-metric-spaces-are-uniformly-continuous.lagda.md +++ b/src/metric-spaces/metrics-of-metric-spaces-are-uniformly-continuous.lagda.md @@ -32,7 +32,7 @@ open import order-theory.large-posets open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.distance-real-numbers -open import real-numbers.inequalities-addition-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-nonnegative-real-numbers open import real-numbers.nonnegative-real-numbers diff --git a/src/metric-spaces/metrics-of-metric-spaces.lagda.md b/src/metric-spaces/metrics-of-metric-spaces.lagda.md index d113ff5bac..271f974d53 100644 --- a/src/metric-spaces/metrics-of-metric-spaces.lagda.md +++ b/src/metric-spaces/metrics-of-metric-spaces.lagda.md @@ -28,7 +28,7 @@ open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.saturation-inequality-nonnegative-real-numbers open import real-numbers.similarity-nonnegative-real-numbers -open import real-numbers.strict-inequalities-addition-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-nonnegative-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 876511f445..3b84f6c0b0 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -23,7 +23,7 @@ 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 open import real-numbers.finitely-enumerable-subsets-real-numbers public -open import real-numbers.inequalities-addition-real-numbers public +open import real-numbers.inequalities-addition-and-subtraction-real-numbers public open import real-numbers.inequality-lower-dedekind-real-numbers public open import real-numbers.inequality-nonnegative-real-numbers public open import real-numbers.inequality-positive-real-numbers public @@ -75,13 +75,13 @@ open import real-numbers.real-numbers-from-lower-dedekind-real-numbers public open import real-numbers.real-numbers-from-upper-dedekind-real-numbers public open import real-numbers.saturation-inequality-nonnegative-real-numbers public open import real-numbers.saturation-inequality-real-numbers public -open import real-numbers.short-binary-maximum-real-numbers public +open import real-numbers.short-function-binary-maximum-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 open import real-numbers.square-roots-nonnegative-real-numbers public open import real-numbers.squares-real-numbers public -open import real-numbers.strict-inequalities-addition-real-numbers public +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers public open import real-numbers.strict-inequality-nonnegative-real-numbers public open import real-numbers.strict-inequality-positive-real-numbers public open import real-numbers.strict-inequality-real-numbers public diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md index ba2031c002..4f77b3aad2 100644 --- a/src/real-numbers/absolute-value-real-numbers.lagda.md +++ b/src/real-numbers/absolute-value-real-numbers.lagda.md @@ -28,7 +28,7 @@ open import metric-spaces.short-functions-metric-spaces open import real-numbers.addition-real-numbers open import real-numbers.binary-maximum-real-numbers open import real-numbers.dedekind-real-numbers -open import real-numbers.inequalities-addition-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.isometry-negation-real-numbers open import real-numbers.metric-space-of-real-numbers diff --git a/src/real-numbers/addition-nonnegative-real-numbers.lagda.md b/src/real-numbers/addition-nonnegative-real-numbers.lagda.md index 0735a72392..5298362a87 100644 --- a/src/real-numbers/addition-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/addition-nonnegative-real-numbers.lagda.md @@ -21,12 +21,12 @@ open import foundation.universe-levels open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers -open import real-numbers.inequalities-addition-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.strict-inequalities-addition-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-nonnegative-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers/binary-maximum-real-numbers.lagda.md b/src/real-numbers/binary-maximum-real-numbers.lagda.md index 69b9224d86..a321c82356 100644 --- a/src/real-numbers/binary-maximum-real-numbers.lagda.md +++ b/src/real-numbers/binary-maximum-real-numbers.lagda.md @@ -28,7 +28,7 @@ open import order-theory.least-upper-bounds-large-posets 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-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.lower-dedekind-real-numbers open import real-numbers.maximum-lower-dedekind-real-numbers diff --git a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md index ab073ba3c2..9d4f3567a1 100644 --- a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md @@ -45,7 +45,7 @@ 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.distance-real-numbers -open import real-numbers.inequalities-addition-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.lower-dedekind-real-numbers open import real-numbers.metric-space-of-real-numbers diff --git a/src/real-numbers/distance-real-numbers.lagda.md b/src/real-numbers/distance-real-numbers.lagda.md index eff38740f5..8e430fb8b0 100644 --- a/src/real-numbers/distance-real-numbers.lagda.md +++ b/src/real-numbers/distance-real-numbers.lagda.md @@ -28,7 +28,7 @@ open import real-numbers.absolute-value-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-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.multiplication-real-numbers diff --git a/src/real-numbers/inequalities-addition-real-numbers.lagda.md b/src/real-numbers/inequalities-addition-and-subtraction-real-numbers.lagda.md similarity index 98% rename from src/real-numbers/inequalities-addition-real-numbers.lagda.md rename to src/real-numbers/inequalities-addition-and-subtraction-real-numbers.lagda.md index b5af4c0787..61de6c5cfb 100644 --- a/src/real-numbers/inequalities-addition-real-numbers.lagda.md +++ b/src/real-numbers/inequalities-addition-and-subtraction-real-numbers.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --lossy-unification #-} -module real-numbers.inequalities-addition-real-numbers where +module real-numbers.inequalities-addition-and-subtraction-real-numbers where ```
Imports diff --git a/src/real-numbers/infima-families-real-numbers.lagda.md b/src/real-numbers/infima-families-real-numbers.lagda.md index add144950d..0b338cbe37 100644 --- a/src/real-numbers/infima-families-real-numbers.lagda.md +++ b/src/real-numbers/infima-families-real-numbers.lagda.md @@ -41,7 +41,7 @@ open import real-numbers.negation-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-inequalities-addition-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 open import real-numbers.suprema-families-real-numbers diff --git a/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md b/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md index 21124540b7..8a3677def8 100644 --- a/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md +++ b/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md @@ -44,7 +44,7 @@ open import real-numbers.cauchy-completeness-dedekind-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.inequalities-addition-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.infima-and-suprema-families-real-numbers @@ -55,7 +55,7 @@ open import real-numbers.metric-space-of-real-numbers open import real-numbers.negation-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.strict-inequalities-addition-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 open import real-numbers.suprema-families-real-numbers diff --git a/src/real-numbers/isometry-addition-real-numbers.lagda.md b/src/real-numbers/isometry-addition-real-numbers.lagda.md index a7d3686d03..c42c49edba 100644 --- a/src/real-numbers/isometry-addition-real-numbers.lagda.md +++ b/src/real-numbers/isometry-addition-real-numbers.lagda.md @@ -24,7 +24,7 @@ open import metric-spaces.uniformly-continuous-functions-metric-spaces open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers -open import real-numbers.inequalities-addition-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.raising-universe-levels-real-numbers diff --git a/src/real-numbers/isometry-negation-real-numbers.lagda.md b/src/real-numbers/isometry-negation-real-numbers.lagda.md index 7e5f7562a2..e36974427a 100644 --- a/src/real-numbers/isometry-negation-real-numbers.lagda.md +++ b/src/real-numbers/isometry-negation-real-numbers.lagda.md @@ -24,7 +24,7 @@ open import metric-spaces.metric-spaces open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers -open import real-numbers.inequalities-addition-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 diff --git a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md index ed960956fe..1b56e2c244 100644 --- a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md +++ b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md @@ -36,7 +36,7 @@ open import real-numbers.arithmetically-located-dedekind-cuts open import real-numbers.dedekind-real-numbers open import real-numbers.distance-real-numbers open import real-numbers.enclosing-closed-rational-intervals-real-numbers -open import real-numbers.inequalities-addition-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.inhabited-totally-bounded-subsets-real-numbers open import real-numbers.metric-space-of-real-numbers diff --git a/src/real-numbers/maximum-finite-families-real-numbers.lagda.md b/src/real-numbers/maximum-finite-families-real-numbers.lagda.md index 5e757a72e7..34e2ed1f44 100644 --- a/src/real-numbers/maximum-finite-families-real-numbers.lagda.md +++ b/src/real-numbers/maximum-finite-families-real-numbers.lagda.md @@ -43,7 +43,7 @@ open import real-numbers.inequality-real-numbers open import real-numbers.negation-real-numbers open import real-numbers.positive-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.strict-inequalities-addition-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.suprema-families-real-numbers 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 d199e3ef54..7d78c3c437 100644 --- a/src/real-numbers/metric-space-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-space-of-real-numbers.lagda.md @@ -44,12 +44,12 @@ open import metric-spaces.triangular-rational-neighborhood-relations 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-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers -open import real-numbers.strict-inequalities-addition-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.transposition-addition-subtraction-cuts-dedekind-real-numbers ``` diff --git a/src/real-numbers/nonnegative-real-numbers.lagda.md b/src/real-numbers/nonnegative-real-numbers.lagda.md index fcb7e126e0..d8219df9e7 100644 --- a/src/real-numbers/nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/nonnegative-real-numbers.lagda.md @@ -36,7 +36,7 @@ open import metric-spaces.metric-spaces 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-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.strict-inequality-real-numbers diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md index 668e1644d9..e32729d0f7 100644 --- a/src/real-numbers/positive-real-numbers.lagda.md +++ b/src/real-numbers/positive-real-numbers.lagda.md @@ -40,7 +40,7 @@ open import real-numbers.negation-real-numbers open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers -open import real-numbers.strict-inequalities-addition-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers/saturation-inequality-real-numbers.lagda.md b/src/real-numbers/saturation-inequality-real-numbers.lagda.md index 437a1a7a32..fad1d8e16c 100644 --- a/src/real-numbers/saturation-inequality-real-numbers.lagda.md +++ b/src/real-numbers/saturation-inequality-real-numbers.lagda.md @@ -21,7 +21,7 @@ open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.strict-inequalities-addition-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers/short-binary-maximum-real-numbers.lagda.md b/src/real-numbers/short-function-binary-maximum-real-numbers.lagda.md similarity index 97% rename from src/real-numbers/short-binary-maximum-real-numbers.lagda.md rename to src/real-numbers/short-function-binary-maximum-real-numbers.lagda.md index 5dd32621e1..9cca40873e 100644 --- a/src/real-numbers/short-binary-maximum-real-numbers.lagda.md +++ b/src/real-numbers/short-function-binary-maximum-real-numbers.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --lossy-unification #-} -module real-numbers.short-binary-maximum-real-numbers where +module real-numbers.short-function-binary-maximum-real-numbers where ```
Imports @@ -23,7 +23,7 @@ open import order-theory.least-upper-bounds-large-posets open import real-numbers.addition-real-numbers open import real-numbers.binary-maximum-real-numbers open import real-numbers.dedekind-real-numbers -open import real-numbers.inequalities-addition-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.positive-real-numbers diff --git a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md b/src/real-numbers/strict-inequalities-addition-and-subtraction-real-numbers.lagda.md similarity index 99% rename from src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md rename to src/real-numbers/strict-inequalities-addition-and-subtraction-real-numbers.lagda.md index 24417dab87..26b7ac1b7d 100644 --- a/src/real-numbers/strict-inequalities-addition-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequalities-addition-and-subtraction-real-numbers.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --lossy-unification #-} -module real-numbers.strict-inequalities-addition-real-numbers where +module real-numbers.strict-inequalities-addition-and-subtraction-real-numbers where ```
Imports diff --git a/src/real-numbers/suprema-families-real-numbers.lagda.md b/src/real-numbers/suprema-families-real-numbers.lagda.md index f730c05498..d51a2e2a29 100644 --- a/src/real-numbers/suprema-families-real-numbers.lagda.md +++ b/src/real-numbers/suprema-families-real-numbers.lagda.md @@ -42,7 +42,7 @@ open import real-numbers.negation-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-inequalities-addition-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 ``` diff --git a/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md b/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md index 91e5c9c0be..82a733d139 100644 --- a/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md @@ -24,7 +24,7 @@ open import real-numbers.difference-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-inequalities-addition-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers ``` From a85cdcbaa33e6a6f4c989c05584e592e304701de Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 12:04:12 -0800 Subject: [PATCH 16/21] Fix --- .../inequality-positive-rational-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md index 5b51936f6a..1398ef233b 100644 --- a/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md @@ -97,5 +97,5 @@ antisymmetric-leq-ℚ⁺ = antisymmetric-leq-Poset poset-ℚ⁺ ```agda leq-eq-ℚ⁺ : {x y : ℚ⁺} → x = y → leq-ℚ⁺ x y -leq-eq-ℚ⁺ x=y = leq-eq-ℚ _ _ (ap rational-ℚ⁺ x=y) +leq-eq-ℚ⁺ x=y = leq-eq-ℚ (ap rational-ℚ⁺ x=y) ``` From 1d5f0a217083dd72cdb145026a765ae94b94b38a Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 12:25:44 -0800 Subject: [PATCH 17/21] Fix --- src/real-numbers/absolute-value-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md index 4f77b3aad2..fc75c7ed59 100644 --- a/src/real-numbers/absolute-value-real-numbers.lagda.md +++ b/src/real-numbers/absolute-value-real-numbers.lagda.md @@ -132,7 +132,7 @@ abstract opaque ( zero-ℝ) ( x) ( 0≤x) - ( tr (leq-ℝ (neg-ℝ x)) neg-zero-ℝ (neg-leq-ℝ _ _ 0≤x)))) + ( tr (leq-ℝ (neg-ℝ x)) neg-zero-ℝ (neg-leq-ℝ 0≤x)))) abs-real-ℝ⁺ : {l : Level} (x : ℝ⁺ l) → abs-ℝ (real-ℝ⁺ x) = real-ℝ⁺ x abs-real-ℝ⁺ x = abs-real-ℝ⁰⁺ (nonnegative-ℝ⁺ x) From 399e3c37bb884b897b35304ec9133218680f5b6f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Nov 2025 12:35:18 -0800 Subject: [PATCH 18/21] Fix build --- .../powers-positive-rational-numbers.lagda.md | 8 ++++---- ...ication-positive-and-negative-real-numbers.lagda.md | 2 +- src/real-numbers/powers-real-numbers.lagda.md | 10 +++++----- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md index 847d6dbbba..05641432b4 100644 --- a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md @@ -294,9 +294,9 @@ abstract ( _) ( preserves-leq-power-ℚ⁺ k ε one-ℚ⁺ ε≤1) ≤ one-ℚ *ℚ rational-power-ℚ⁺ m ε - by leq-eq-ℚ _ _ (ap-mul-ℚ (ap rational-ℚ⁺ (power-one-ℚ⁺ k)) refl) + by leq-eq-ℚ (ap-mul-ℚ (ap rational-ℚ⁺ (power-one-ℚ⁺ k)) refl) ≤ rational-power-ℚ⁺ m ε - by leq-eq-ℚ _ _ (left-unit-law-mul-ℚ _) + by leq-eq-ℚ (left-unit-law-mul-ℚ _) ``` ### If `ε` is a positive rational number less than 1, `εⁿ` approaches 0 @@ -327,10 +327,10 @@ abstract rational-dist-ℚ (rational-ℚ⁺ (power-ℚ⁺ n ε)) zero-ℚ ≤ rational-abs-ℚ (rational-ℚ⁺ (power-ℚ⁺ n ε)) by - leq-eq-ℚ _ _ (ap rational-ℚ⁰⁺ (right-zero-law-dist-ℚ _)) + leq-eq-ℚ (ap rational-ℚ⁰⁺ (right-zero-law-dist-ℚ _)) ≤ rational-ℚ⁺ (power-ℚ⁺ n ε) by - leq-eq-ℚ _ _ + leq-eq-ℚ ( ap rational-ℚ⁰⁺ ( abs-rational-ℚ⁰⁺ (nonnegative-ℚ⁺ (power-ℚ⁺ n ε)))) ≤ rational-ℚ⁺ (power-ℚ⁺ m ε) diff --git a/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md b/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md index 7ecc0768e3..c0fea89695 100644 --- a/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md @@ -44,7 +44,7 @@ abstract ( x *ℝ zero-ℝ) ( zero-ℝ) ( right-zero-law-mul-ℝ x) - ( preserves-le-left-mul-ℝ⁺ (x , is-pos-x) y zero-ℝ is-neg-y) + ( preserves-le-left-mul-ℝ⁺ (x , is-pos-x) is-neg-y) mul-positive-negative-ℝ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁻ l2 → ℝ⁻ (l1 ⊔ l2) diff --git a/src/real-numbers/powers-real-numbers.lagda.md b/src/real-numbers/powers-real-numbers.lagda.md index 497f3b7c04..8038140ac0 100644 --- a/src/real-numbers/powers-real-numbers.lagda.md +++ b/src/real-numbers/powers-real-numbers.lagda.md @@ -293,7 +293,7 @@ abstract {l1 l2 : Level} (n : ℕ) (x : ℝ l1) (y : ℝ l2) → leq-ℝ (abs-ℝ x) (abs-ℝ y) → leq-ℝ (abs-ℝ (power-ℝ n x)) (abs-ℝ (power-ℝ n y)) preserves-leq-abs-power-ℝ 0 _ _ _ = - preserves-leq-sim-ℝ _ _ _ _ + preserves-leq-sim-ℝ ( inv-tr ( sim-ℝ one-ℝ) ( abs-real-ℝ⁺ (raise-ℝ⁺ _ one-ℝ⁺)) @@ -310,9 +310,9 @@ abstract chain-of-inequalities abs-ℝ (power-ℝ (succ-ℕ n) x) ≤ abs-ℝ (power-ℝ n x *ℝ x) - by leq-eq-ℝ _ _ (ap abs-ℝ (power-succ-ℝ n x)) + by leq-eq-ℝ (ap abs-ℝ (power-succ-ℝ n x)) ≤ abs-ℝ (power-ℝ n x) *ℝ abs-ℝ x - by leq-eq-ℝ _ _ (abs-mul-ℝ _ _) + by leq-eq-ℝ (abs-mul-ℝ _ _) ≤ abs-ℝ (power-ℝ n y) *ℝ abs-ℝ y by preserves-leq-mul-ℝ⁰⁺ @@ -323,7 +323,7 @@ abstract ( preserves-leq-abs-power-ℝ n x y |x|≤|y|) ( |x|≤|y|) ≤ abs-ℝ (power-ℝ n y *ℝ y) - by leq-eq-ℝ _ _ (inv (abs-mul-ℝ _ _)) + by leq-eq-ℝ (inv (abs-mul-ℝ _ _)) ≤ abs-ℝ (power-ℝ (succ-ℕ n) y) - by leq-eq-ℝ _ _ (ap abs-ℝ (inv (power-succ-ℝ n y))) + by leq-eq-ℝ (ap abs-ℝ (inv (power-succ-ℝ n y))) ``` From 8569df8582c3d35496e39a140b7ed34d00d965cd Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 9 Nov 2025 13:06:21 +0100 Subject: [PATCH 19/21] chore: optimize imports `real-numbers` --- src/real-numbers/absolute-value-real-numbers.lagda.md | 1 - .../addition-lower-dedekind-real-numbers.lagda.md | 5 ----- .../addition-nonnegative-real-numbers.lagda.md | 1 - src/real-numbers/addition-real-numbers.lagda.md | 1 - .../addition-upper-dedekind-real-numbers.lagda.md | 2 -- src/real-numbers/apartness-real-numbers.lagda.md | 3 --- .../arithmetically-located-dedekind-cuts.lagda.md | 2 -- src/real-numbers/binary-maximum-real-numbers.lagda.md | 2 -- ...cauchy-completeness-dedekind-real-numbers.lagda.md | 4 ---- .../cauchy-sequences-real-numbers.lagda.md | 4 ---- .../closed-intervals-real-numbers.lagda.md | 4 ---- src/real-numbers/dedekind-real-numbers.lagda.md | 9 --------- src/real-numbers/difference-real-numbers.lagda.md | 1 - src/real-numbers/distance-real-numbers.lagda.md | 2 -- ...ng-closed-rational-intervals-real-numbers.lagda.md | 1 - .../inequality-nonnegative-real-numbers.lagda.md | 1 - .../inequality-positive-real-numbers.lagda.md | 1 - .../inequality-upper-dedekind-real-numbers.lagda.md | 1 - .../infima-and-suprema-families-real-numbers.lagda.md | 2 -- ...-finitely-enumerable-subsets-real-numbers.lagda.md | 1 - ...ited-totally-bounded-subsets-real-numbers.lagda.md | 1 - .../isometry-addition-real-numbers.lagda.md | 5 ----- .../isometry-negation-real-numbers.lagda.md | 1 - .../large-additive-group-of-real-numbers.lagda.md | 2 -- ...rge-multiplicative-monoid-of-real-numbers.lagda.md | 2 -- src/real-numbers/large-ring-of-real-numbers.lagda.md | 4 ---- .../limits-sequences-real-numbers.lagda.md | 2 -- ...tz-continuity-multiplication-real-numbers.lagda.md | 7 ------- src/real-numbers/lower-dedekind-real-numbers.lagda.md | 1 - .../maximum-finite-families-real-numbers.lagda.md | 3 --- .../maximum-upper-dedekind-real-numbers.lagda.md | 6 ------ ...-finitely-enumerable-subsets-real-numbers.lagda.md | 3 --- .../minimum-lower-dedekind-real-numbers.lagda.md | 1 - .../minimum-upper-dedekind-real-numbers.lagda.md | 2 -- .../multiplication-nonnegative-real-numbers.lagda.md | 1 - ...cation-positive-and-negative-real-numbers.lagda.md | 1 - .../multiplication-positive-real-numbers.lagda.md | 1 - ...iplicative-inverses-negative-real-numbers.lagda.md | 1 - ...tiplicative-inverses-nonzero-real-numbers.lagda.md | 4 ---- ...iplicative-inverses-positive-real-numbers.lagda.md | 3 --- src/real-numbers/negative-real-numbers.lagda.md | 1 - src/real-numbers/nonnegative-real-numbers.lagda.md | 2 -- .../positive-and-negative-real-numbers.lagda.md | 3 --- src/real-numbers/positive-real-numbers.lagda.md | 9 --------- src/real-numbers/powers-real-numbers.lagda.md | 1 - .../raising-universe-levels-real-numbers.lagda.md | 3 --- src/real-numbers/rational-real-numbers.lagda.md | 11 ----------- ...-numbers-from-lower-dedekind-real-numbers.lagda.md | 3 --- ...-numbers-from-upper-dedekind-real-numbers.lagda.md | 3 --- .../similarity-nonnegative-real-numbers.lagda.md | 7 ------- src/real-numbers/similarity-real-numbers.lagda.md | 9 --------- src/real-numbers/squares-real-numbers.lagda.md | 7 ------- ...ies-addition-and-subtraction-real-numbers.lagda.md | 2 -- ...trict-inequality-nonnegative-real-numbers.lagda.md | 1 - .../strict-inequality-positive-real-numbers.lagda.md | 1 - .../strict-inequality-real-numbers.lagda.md | 1 - src/real-numbers/subsets-real-numbers.lagda.md | 3 --- .../totally-bounded-subsets-real-numbers.lagda.md | 3 --- ...on-subtraction-cuts-dedekind-real-numbers.lagda.md | 1 - src/real-numbers/upper-dedekind-real-numbers.lagda.md | 1 - 60 files changed, 171 deletions(-) diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md index fc75c7ed59..1956f14116 100644 --- a/src/real-numbers/absolute-value-real-numbers.lagda.md +++ b/src/real-numbers/absolute-value-real-numbers.lagda.md @@ -19,7 +19,6 @@ open import foundation.disjunction open import foundation.empty-types open import foundation.function-types open import foundation.identity-types -open import foundation.logical-equivalences open import foundation.transport-along-identifications open import foundation.universe-levels diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index bd1e58abfe..6b2493249e 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -21,27 +21,22 @@ 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.logical-equivalences open import foundation.propositional-truncations -open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import group-theory.abelian-groups open import group-theory.commutative-monoids open import group-theory.groups open import group-theory.minkowski-multiplication-commutative-monoids open import group-theory.monoids open import group-theory.semigroups -open import logic.functoriality-existential-quantification - open import real-numbers.lower-dedekind-real-numbers open import real-numbers.rational-lower-dedekind-real-numbers ``` diff --git a/src/real-numbers/addition-nonnegative-real-numbers.lagda.md b/src/real-numbers/addition-nonnegative-real-numbers.lagda.md index 5298362a87..6c29699df8 100644 --- a/src/real-numbers/addition-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/addition-nonnegative-real-numbers.lagda.md @@ -28,7 +28,6 @@ open import real-numbers.nonnegative-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-nonnegative-real-numbers -open import real-numbers.strict-inequality-real-numbers ```
diff --git a/src/real-numbers/addition-real-numbers.lagda.md b/src/real-numbers/addition-real-numbers.lagda.md index 356d51654f..8f67041ac9 100644 --- a/src/real-numbers/addition-real-numbers.lagda.md +++ b/src/real-numbers/addition-real-numbers.lagda.md @@ -11,7 +11,6 @@ module real-numbers.addition-real-numbers where ```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 diff --git a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md index 616124b951..7ada6a30a2 100644 --- a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md @@ -19,7 +19,6 @@ 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 @@ -30,7 +29,6 @@ open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import group-theory.abelian-groups open import group-theory.commutative-monoids open import group-theory.groups open import group-theory.minkowski-multiplication-commutative-monoids diff --git a/src/real-numbers/apartness-real-numbers.lagda.md b/src/real-numbers/apartness-real-numbers.lagda.md index 023123e63e..242133133b 100644 --- a/src/real-numbers/apartness-real-numbers.lagda.md +++ b/src/real-numbers/apartness-real-numbers.lagda.md @@ -7,18 +7,15 @@ module real-numbers.apartness-real-numbers where
Imports ```agda -open import foundation.apartness-relations open import foundation.disjunction open import foundation.empty-types open import foundation.function-types open import foundation.functoriality-disjunction -open import foundation.identity-types open import foundation.large-apartness-relations open import foundation.large-binary-relations open import foundation.negated-equality open import foundation.negation open import foundation.propositions -open import foundation.transport-along-identifications open import foundation.universe-levels open import real-numbers.dedekind-real-numbers diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 1592876b21..d2abf4e12a 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -27,7 +27,6 @@ open import elementary-number-theory.strict-inequality-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.coproduct-types @@ -37,7 +36,6 @@ open import foundation.empty-types open import foundation.existential-quantification open import foundation.function-types open import foundation.identity-types -open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes diff --git a/src/real-numbers/binary-maximum-real-numbers.lagda.md b/src/real-numbers/binary-maximum-real-numbers.lagda.md index a321c82356..d4da7d69c0 100644 --- a/src/real-numbers/binary-maximum-real-numbers.lagda.md +++ b/src/real-numbers/binary-maximum-real-numbers.lagda.md @@ -25,10 +25,8 @@ open import order-theory.join-semilattices open import order-theory.large-join-semilattices open import order-theory.least-upper-bounds-large-posets -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.lower-dedekind-real-numbers open import real-numbers.maximum-lower-dedekind-real-numbers diff --git a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md index 9d4f3567a1..6e102ad464 100644 --- a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md @@ -21,7 +21,6 @@ open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.dependent-pair-types -open import foundation.disjunction open import foundation.empty-types open import foundation.existential-quantification open import foundation.functoriality-disjunction @@ -34,19 +33,16 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cauchy-approximations-metric-spaces -open import metric-spaces.cauchy-sequences-complete-metric-spaces open import metric-spaces.complete-metric-spaces open import metric-spaces.convergent-cauchy-approximations-metric-spaces open import metric-spaces.limits-of-cauchy-approximations-metric-spaces open import metric-spaces.metric-spaces -open import real-numbers.absolute-value-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.distance-real-numbers open import real-numbers.inequalities-addition-and-subtraction-real-numbers -open import real-numbers.inequality-real-numbers open import real-numbers.lower-dedekind-real-numbers open import real-numbers.metric-space-of-real-numbers open import real-numbers.negation-real-numbers diff --git a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md index cac5f34c62..6876201386 100644 --- a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md +++ b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md @@ -11,14 +11,10 @@ module real-numbers.cauchy-sequences-real-numbers where ```agda open import foundation.universe-levels -open import lists.sequences - open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.cauchy-sequences-complete-metric-spaces open import metric-spaces.cauchy-sequences-metric-spaces -open import metric-spaces.convergent-sequences-metric-spaces -open import real-numbers.addition-real-numbers open import real-numbers.cauchy-completeness-dedekind-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.isometry-addition-real-numbers diff --git a/src/real-numbers/closed-intervals-real-numbers.lagda.md b/src/real-numbers/closed-intervals-real-numbers.lagda.md index d8460f5bdc..09d4fada9e 100644 --- a/src/real-numbers/closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/closed-intervals-real-numbers.lagda.md @@ -11,9 +11,6 @@ open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.positive-rational-numbers -open import elementary-number-theory.rational-numbers -open import elementary-number-theory.strict-inequality-positive-rational-numbers -open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.dependent-pair-types open import foundation.logical-equivalences @@ -26,7 +23,6 @@ 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.subspaces-metric-spaces open import order-theory.closed-intervals-large-posets diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index d846a3556d..22ece70191 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -15,8 +15,6 @@ 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.complements-subtypes open import foundation.conjunction open import foundation.coproduct-types open import foundation.dependent-pair-types @@ -24,28 +22,21 @@ open import foundation.disjoint-subtypes open import foundation.disjunction open import foundation.embeddings open import foundation.empty-types -open import foundation.equivalences open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types -open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.negation -open import foundation.powersets -open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.similarity-subtypes open import foundation.subtypes open import foundation.transport-along-identifications -open import foundation.truncated-types open import foundation.universal-quantification open import foundation.universe-levels -open import foundation-core.truncation-levels - open import logic.functoriality-existential-quantification open import real-numbers.lower-dedekind-real-numbers diff --git a/src/real-numbers/difference-real-numbers.lagda.md b/src/real-numbers/difference-real-numbers.lagda.md index e3a1cd036e..0d13f8b33f 100644 --- a/src/real-numbers/difference-real-numbers.lagda.md +++ b/src/real-numbers/difference-real-numbers.lagda.md @@ -14,7 +14,6 @@ open import elementary-number-theory.rational-numbers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions -open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels diff --git a/src/real-numbers/distance-real-numbers.lagda.md b/src/real-numbers/distance-real-numbers.lagda.md index 8e430fb8b0..4bc37c1536 100644 --- a/src/real-numbers/distance-real-numbers.lagda.md +++ b/src/real-numbers/distance-real-numbers.lagda.md @@ -9,11 +9,9 @@ module real-numbers.distance-real-numbers where
Imports ```agda -open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.positive-rational-numbers -open import elementary-number-theory.rational-numbers open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types diff --git a/src/real-numbers/enclosing-closed-rational-intervals-real-numbers.lagda.md b/src/real-numbers/enclosing-closed-rational-intervals-real-numbers.lagda.md index 77d3ab8c6b..977e33b224 100644 --- a/src/real-numbers/enclosing-closed-rational-intervals-real-numbers.lagda.md +++ b/src/real-numbers/enclosing-closed-rational-intervals-real-numbers.lagda.md @@ -10,7 +10,6 @@ module real-numbers.enclosing-closed-rational-intervals-real-numbers where open import elementary-number-theory.closed-intervals-rational-numbers open import elementary-number-theory.interior-closed-intervals-rational-numbers open import elementary-number-theory.intersections-closed-intervals-rational-numbers -open import elementary-number-theory.rational-numbers open import foundation.conjunction open import foundation.dependent-pair-types diff --git a/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md b/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md index fa71aea44a..dc71c190c0 100644 --- a/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md @@ -22,7 +22,6 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels -open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.rational-real-numbers diff --git a/src/real-numbers/inequality-positive-real-numbers.lagda.md b/src/real-numbers/inequality-positive-real-numbers.lagda.md index 2ef1d3a686..15343cc094 100644 --- a/src/real-numbers/inequality-positive-real-numbers.lagda.md +++ b/src/real-numbers/inequality-positive-real-numbers.lagda.md @@ -12,7 +12,6 @@ module real-numbers.inequality-positive-real-numbers where open import foundation.propositions open import foundation.universe-levels -open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.positive-real-numbers ``` diff --git a/src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md index 2b8a3de889..48dc2d04d4 100644 --- a/src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md @@ -18,7 +18,6 @@ open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.existential-quantification open import foundation.logical-equivalences -open import foundation.powersets open import foundation.propositions open import foundation.subtypes open import foundation.unit-type diff --git a/src/real-numbers/infima-and-suprema-families-real-numbers.lagda.md b/src/real-numbers/infima-and-suprema-families-real-numbers.lagda.md index f889ec1a31..6a0b26fdf4 100644 --- a/src/real-numbers/infima-and-suprema-families-real-numbers.lagda.md +++ b/src/real-numbers/infima-and-suprema-families-real-numbers.lagda.md @@ -8,7 +8,6 @@ module real-numbers.infima-and-suprema-families-real-numbers where ```agda open import foundation.dependent-pair-types -open import foundation.existential-quantification open import foundation.propositional-truncations open import foundation.subtypes open import foundation.universe-levels @@ -17,7 +16,6 @@ open import real-numbers.closed-intervals-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.infima-families-real-numbers -open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.subsets-real-numbers open import real-numbers.suprema-families-real-numbers ``` diff --git a/src/real-numbers/inhabited-finitely-enumerable-subsets-real-numbers.lagda.md b/src/real-numbers/inhabited-finitely-enumerable-subsets-real-numbers.lagda.md index 945abdb69c..a5eb36703a 100644 --- a/src/real-numbers/inhabited-finitely-enumerable-subsets-real-numbers.lagda.md +++ b/src/real-numbers/inhabited-finitely-enumerable-subsets-real-numbers.lagda.md @@ -20,7 +20,6 @@ open import real-numbers.negation-real-numbers open import real-numbers.subsets-real-numbers open import univalent-combinatorics.finitely-enumerable-subtypes -open import univalent-combinatorics.finitely-enumerable-types open import univalent-combinatorics.inhabited-finitely-enumerable-subtypes ``` diff --git a/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md b/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md index 8a3677def8..3b65a9823d 100644 --- a/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md +++ b/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md @@ -32,7 +32,6 @@ open import metric-spaces.approximations-metric-spaces open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.nets-metric-spaces -open import metric-spaces.subspaces-metric-spaces open import metric-spaces.totally-bounded-metric-spaces open import order-theory.upper-bounds-large-posets diff --git a/src/real-numbers/isometry-addition-real-numbers.lagda.md b/src/real-numbers/isometry-addition-real-numbers.lagda.md index c42c49edba..3b1ca98943 100644 --- a/src/real-numbers/isometry-addition-real-numbers.lagda.md +++ b/src/real-numbers/isometry-addition-real-numbers.lagda.md @@ -11,25 +11,20 @@ module real-numbers.isometry-addition-real-numbers where ```agda open import foundation.dependent-pair-types open import foundation.function-extensionality -open import foundation.function-types open import foundation.transport-along-identifications open import foundation.universe-levels 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.metric-spaces open import metric-spaces.modulated-uniformly-continuous-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 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.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.strict-inequality-real-numbers ```
diff --git a/src/real-numbers/isometry-negation-real-numbers.lagda.md b/src/real-numbers/isometry-negation-real-numbers.lagda.md index e36974427a..3c2b449432 100644 --- a/src/real-numbers/isometry-negation-real-numbers.lagda.md +++ b/src/real-numbers/isometry-negation-real-numbers.lagda.md @@ -20,7 +20,6 @@ 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 real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers diff --git a/src/real-numbers/large-additive-group-of-real-numbers.lagda.md b/src/real-numbers/large-additive-group-of-real-numbers.lagda.md index 77808a473a..8e876af34b 100644 --- a/src/real-numbers/large-additive-group-of-real-numbers.lagda.md +++ b/src/real-numbers/large-additive-group-of-real-numbers.lagda.md @@ -9,10 +9,8 @@ module real-numbers.large-additive-group-of-real-numbers where
Imports ```agda -open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers -open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels diff --git a/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md b/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md index 87f9524dc3..b5d2a73c59 100644 --- a/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md +++ b/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md @@ -11,9 +11,7 @@ module real-numbers.large-multiplicative-monoid-of-real-numbers where ```agda open import foundation.universe-levels -open import group-theory.abelian-groups open import group-theory.commutative-monoids -open import group-theory.large-abelian-groups open import group-theory.large-commutative-monoids open import group-theory.large-monoids open import group-theory.large-semigroups diff --git a/src/real-numbers/large-ring-of-real-numbers.lagda.md b/src/real-numbers/large-ring-of-real-numbers.lagda.md index 5786d7c56c..98fd1e8782 100644 --- a/src/real-numbers/large-ring-of-real-numbers.lagda.md +++ b/src/real-numbers/large-ring-of-real-numbers.lagda.md @@ -13,16 +13,12 @@ open import commutative-algebra.commutative-rings open import commutative-algebra.homomorphisms-commutative-rings open import commutative-algebra.large-commutative-rings -open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.ring-of-rational-numbers -open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels -open import group-theory.large-monoids - open import real-numbers.large-additive-group-of-real-numbers open import real-numbers.multiplication-real-numbers open import real-numbers.raising-universe-levels-real-numbers diff --git a/src/real-numbers/limits-sequences-real-numbers.lagda.md b/src/real-numbers/limits-sequences-real-numbers.lagda.md index f40aab460f..f7ab605183 100644 --- a/src/real-numbers/limits-sequences-real-numbers.lagda.md +++ b/src/real-numbers/limits-sequences-real-numbers.lagda.md @@ -10,7 +10,6 @@ module real-numbers.limits-sequences-real-numbers where ```agda open import foundation.dependent-pair-types -open import foundation.propositional-truncations open import foundation.universe-levels open import lists.sequences @@ -19,7 +18,6 @@ open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.limits-of-sequences-metric-spaces open import real-numbers.addition-real-numbers -open import real-numbers.cauchy-sequences-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.isometry-addition-real-numbers open import real-numbers.metric-space-of-real-numbers diff --git a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md index 1b56e2c244..b44914841b 100644 --- a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md +++ b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md @@ -12,14 +12,10 @@ module real-numbers.lipschitz-continuity-multiplication-real-numbers where open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers -open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.existential-quantification -open import foundation.function-extensionality open import foundation.identity-types -open import foundation.logical-equivalences open import foundation.propositional-truncations -open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cartesian-products-metric-spaces @@ -28,14 +24,11 @@ open import metric-spaces.uniformly-continuous-functions-metric-spaces open import order-theory.large-posets -open import real-numbers.absolute-value-closed-intervals-real-numbers open import real-numbers.absolute-value-real-numbers open import real-numbers.addition-nonnegative-real-numbers open import real-numbers.addition-real-numbers -open import real-numbers.arithmetically-located-dedekind-cuts open import real-numbers.dedekind-real-numbers open import real-numbers.distance-real-numbers -open import real-numbers.enclosing-closed-rational-intervals-real-numbers open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.inhabited-totally-bounded-subsets-real-numbers diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index 6cfa5efab4..0372e6da37 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -24,7 +24,6 @@ open import foundation.existential-quantification open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences -open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.similarity-subtypes diff --git a/src/real-numbers/maximum-finite-families-real-numbers.lagda.md b/src/real-numbers/maximum-finite-families-real-numbers.lagda.md index 34e2ed1f44..543950300e 100644 --- a/src/real-numbers/maximum-finite-families-real-numbers.lagda.md +++ b/src/real-numbers/maximum-finite-families-real-numbers.lagda.md @@ -9,7 +9,6 @@ module real-numbers.maximum-finite-families-real-numbers where ```agda open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.natural-numbers -open import elementary-number-theory.positive-rational-numbers open import foundation.action-on-identifications-functions open import foundation.coproduct-types @@ -30,7 +29,6 @@ open import lists.finite-sequences open import logic.functoriality-existential-quantification -open import order-theory.join-semilattices open import order-theory.joins-finite-families-join-semilattices open import order-theory.least-upper-bounds-large-posets open import order-theory.upper-bounds-large-posets @@ -40,7 +38,6 @@ open import real-numbers.binary-maximum-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.negation-real-numbers open import real-numbers.positive-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers diff --git a/src/real-numbers/maximum-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/maximum-upper-dedekind-real-numbers.lagda.md index b4eb768f8b..8819476f7c 100644 --- a/src/real-numbers/maximum-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/maximum-upper-dedekind-real-numbers.lagda.md @@ -16,15 +16,9 @@ open import elementary-number-theory.strict-inequality-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.function-types -open import foundation.functoriality-cartesian-product-types -open import foundation.inhabited-types open import foundation.intersections-subtypes open import foundation.logical-equivalences -open import foundation.powersets -open import foundation.propositional-truncations open import foundation.subtypes open import foundation.universe-levels diff --git a/src/real-numbers/minimum-inhabited-finitely-enumerable-subsets-real-numbers.lagda.md b/src/real-numbers/minimum-inhabited-finitely-enumerable-subsets-real-numbers.lagda.md index 5909da62ca..57f9d1bf80 100644 --- a/src/real-numbers/minimum-inhabited-finitely-enumerable-subsets-real-numbers.lagda.md +++ b/src/real-numbers/minimum-inhabited-finitely-enumerable-subsets-real-numbers.lagda.md @@ -21,9 +21,6 @@ open import real-numbers.infima-families-real-numbers open import real-numbers.inhabited-finitely-enumerable-subsets-real-numbers open import real-numbers.maximum-inhabited-finitely-enumerable-subsets-real-numbers open import real-numbers.negation-real-numbers -open import real-numbers.subsets-real-numbers - -open import univalent-combinatorics.finitely-enumerable-subtypes ```
diff --git a/src/real-numbers/minimum-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/minimum-lower-dedekind-real-numbers.lagda.md index 860e3cee2a..e0c6900799 100644 --- a/src/real-numbers/minimum-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/minimum-lower-dedekind-real-numbers.lagda.md @@ -26,7 +26,6 @@ open import logic.functoriality-existential-quantification open import order-theory.greatest-lower-bounds-large-posets open import order-theory.large-meet-semilattices -open import order-theory.lower-bounds-large-posets open import real-numbers.inequality-lower-dedekind-real-numbers open import real-numbers.lower-dedekind-real-numbers diff --git a/src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md index 590cb5a2e9..6ea8a8c76e 100644 --- a/src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md @@ -21,7 +21,6 @@ open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-disjunction open import foundation.inhabited-types open import foundation.logical-equivalences -open import foundation.powersets open import foundation.propositional-truncations open import foundation.subtypes open import foundation.unions-subtypes @@ -30,7 +29,6 @@ open import foundation.universe-levels open import logic.functoriality-existential-quantification open import order-theory.greatest-lower-bounds-large-posets -open import order-theory.large-inflattices open import order-theory.lower-bounds-large-posets open import real-numbers.inequality-upper-dedekind-real-numbers diff --git a/src/real-numbers/multiplication-nonnegative-real-numbers.lagda.md b/src/real-numbers/multiplication-nonnegative-real-numbers.lagda.md index a1bb60ef8e..b4af60d1c5 100644 --- a/src/real-numbers/multiplication-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-nonnegative-real-numbers.lagda.md @@ -26,7 +26,6 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import real-numbers.dedekind-real-numbers -open import real-numbers.difference-real-numbers open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.multiplication-real-numbers diff --git a/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md b/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md index c0fea89695..9e9e66cc37 100644 --- a/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md @@ -8,7 +8,6 @@ module real-numbers.multiplication-positive-and-negative-real-numbers where ```agda open import foundation.dependent-pair-types -open import foundation.transport-along-identifications open import foundation.universe-levels open import real-numbers.dedekind-real-numbers diff --git a/src/real-numbers/multiplication-positive-real-numbers.lagda.md b/src/real-numbers/multiplication-positive-real-numbers.lagda.md index 7972741f76..c151f0ecd2 100644 --- a/src/real-numbers/multiplication-positive-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-positive-real-numbers.lagda.md @@ -9,7 +9,6 @@ module real-numbers.multiplication-positive-real-numbers where
Imports ```agda -open import elementary-number-theory.closed-intervals-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.minimum-positive-rational-numbers open import elementary-number-theory.multiplication-closed-intervals-rational-numbers diff --git a/src/real-numbers/multiplicative-inverses-negative-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-negative-real-numbers.lagda.md index 8acc9d09e7..564230fd9b 100644 --- a/src/real-numbers/multiplicative-inverses-negative-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-negative-real-numbers.lagda.md @@ -17,7 +17,6 @@ open import foundation.universe-levels open import real-numbers.dedekind-real-numbers open import real-numbers.multiplication-real-numbers open import real-numbers.multiplicative-inverses-positive-real-numbers -open import real-numbers.negation-real-numbers open import real-numbers.negative-real-numbers open import real-numbers.positive-and-negative-real-numbers open import real-numbers.rational-real-numbers diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md index f91c1d2bfc..ad287640f8 100644 --- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md @@ -19,23 +19,19 @@ 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.action-on-identifications-functions open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.empty-types open import foundation.existential-quantification open import foundation.identity-types -open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.transport-along-identifications -open import foundation.unit-type open import foundation.universe-levels open import real-numbers.dedekind-real-numbers -open import real-numbers.inequality-real-numbers open import real-numbers.multiplication-real-numbers open import real-numbers.multiplicative-inverses-negative-real-numbers open import real-numbers.multiplicative-inverses-positive-real-numbers diff --git a/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md index 490dd19044..47b08b6c2a 100644 --- a/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md @@ -12,9 +12,7 @@ module real-numbers.multiplicative-inverses-positive-real-numbers where open import elementary-number-theory.closed-intervals-rational-numbers open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.inequality-rational-numbers -open import elementary-number-theory.maximum-positive-rational-numbers open import elementary-number-theory.maximum-rational-numbers -open import elementary-number-theory.minimum-positive-rational-numbers open import elementary-number-theory.minimum-rational-numbers open import elementary-number-theory.multiplication-closed-intervals-rational-numbers open import elementary-number-theory.multiplication-positive-and-negative-rational-numbers @@ -39,7 +37,6 @@ open import foundation.empty-types open import foundation.equivalences open import foundation.existential-quantification open import foundation.function-types -open import foundation.functoriality-cartesian-product-types open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.logical-equivalences diff --git a/src/real-numbers/negative-real-numbers.lagda.md b/src/real-numbers/negative-real-numbers.lagda.md index fd87ef7b8c..75b3944778 100644 --- a/src/real-numbers/negative-real-numbers.lagda.md +++ b/src/real-numbers/negative-real-numbers.lagda.md @@ -10,7 +10,6 @@ module real-numbers.negative-real-numbers where ```agda open import elementary-number-theory.negative-rational-numbers -open import elementary-number-theory.rational-numbers open import foundation.dependent-pair-types open import foundation.existential-quantification diff --git a/src/real-numbers/nonnegative-real-numbers.lagda.md b/src/real-numbers/nonnegative-real-numbers.lagda.md index d8219df9e7..c7b56ff0af 100644 --- a/src/real-numbers/nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/nonnegative-real-numbers.lagda.md @@ -31,8 +31,6 @@ open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import metric-spaces.metric-spaces - open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers diff --git a/src/real-numbers/positive-and-negative-real-numbers.lagda.md b/src/real-numbers/positive-and-negative-real-numbers.lagda.md index 850496dd46..d1d0920e34 100644 --- a/src/real-numbers/positive-and-negative-real-numbers.lagda.md +++ b/src/real-numbers/positive-and-negative-real-numbers.lagda.md @@ -10,13 +10,10 @@ module real-numbers.positive-and-negative-real-numbers where ```agda open import foundation.dependent-pair-types -open import foundation.identity-types -open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels open import real-numbers.dedekind-real-numbers -open import real-numbers.inequality-real-numbers open import real-numbers.negation-real-numbers open import real-numbers.negative-real-numbers open import real-numbers.nonnegative-real-numbers diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md index e32729d0f7..9b8c6101ca 100644 --- a/src/real-numbers/positive-real-numbers.lagda.md +++ b/src/real-numbers/positive-real-numbers.lagda.md @@ -9,31 +9,22 @@ module real-numbers.positive-real-numbers where
Imports ```agda -open import elementary-number-theory.addition-rational-numbers -open import elementary-number-theory.additive-group-of-rational-numbers -open import elementary-number-theory.difference-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.binary-transport open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.logical-equivalences -open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import group-theory.abelian-groups -open import group-theory.groups - open import real-numbers.addition-real-numbers -open import real-numbers.arithmetically-located-dedekind-cuts open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers open import real-numbers.negation-real-numbers diff --git a/src/real-numbers/powers-real-numbers.lagda.md b/src/real-numbers/powers-real-numbers.lagda.md index 8038140ac0..55ff07d63d 100644 --- a/src/real-numbers/powers-real-numbers.lagda.md +++ b/src/real-numbers/powers-real-numbers.lagda.md @@ -22,7 +22,6 @@ open import elementary-number-theory.ring-of-rational-numbers open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types -open import foundation.disjunction open import foundation.identity-types open import foundation.transport-along-identifications open import foundation.universe-levels diff --git a/src/real-numbers/raising-universe-levels-real-numbers.lagda.md b/src/real-numbers/raising-universe-levels-real-numbers.lagda.md index 2782e63dab..c3f1b1d417 100644 --- a/src/real-numbers/raising-universe-levels-real-numbers.lagda.md +++ b/src/real-numbers/raising-universe-levels-real-numbers.lagda.md @@ -28,9 +28,6 @@ open import foundation.universe-levels open import logic.functoriality-existential-quantification -open import metric-spaces.isometries-metric-spaces -open import metric-spaces.metric-space-of-rational-numbers - open import real-numbers.dedekind-real-numbers open import real-numbers.lower-dedekind-real-numbers open import real-numbers.similarity-real-numbers diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index df01919a62..285729c4a4 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -9,7 +9,6 @@ module real-numbers.rational-real-numbers where
Imports ```agda -open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.integers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.positive-rational-numbers @@ -17,20 +16,14 @@ open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions -open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.disjunction -open import foundation.embeddings open import foundation.empty-types open import foundation.equivalences -open import foundation.existential-quantification open import foundation.function-types -open import foundation.homotopies open import foundation.identity-types -open import foundation.logical-equivalences open import foundation.negation -open import foundation.propositional-truncations open import foundation.propositions open import foundation.retractions open import foundation.sections @@ -38,15 +31,11 @@ open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import logic.functoriality-existential-quantification - open import real-numbers.dedekind-real-numbers -open import real-numbers.lower-dedekind-real-numbers open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-lower-dedekind-real-numbers open import real-numbers.rational-upper-dedekind-real-numbers open import real-numbers.similarity-real-numbers -open import real-numbers.upper-dedekind-real-numbers ```
diff --git a/src/real-numbers/real-numbers-from-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/real-numbers-from-lower-dedekind-real-numbers.lagda.md index 227fa5c7af..1f1c549e9a 100644 --- a/src/real-numbers/real-numbers-from-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/real-numbers-from-lower-dedekind-real-numbers.lagda.md @@ -9,8 +9,6 @@ module real-numbers.real-numbers-from-lower-dedekind-real-numbers where
Imports ```agda -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 @@ -27,7 +25,6 @@ open import foundation.inhabited-subtypes open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations -open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels diff --git a/src/real-numbers/real-numbers-from-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/real-numbers-from-upper-dedekind-real-numbers.lagda.md index 80c6cacfa9..d1d478c1a3 100644 --- a/src/real-numbers/real-numbers-from-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/real-numbers-from-upper-dedekind-real-numbers.lagda.md @@ -9,8 +9,6 @@ module real-numbers.real-numbers-from-upper-dedekind-real-numbers where
Imports ```agda -open import elementary-number-theory.difference-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 @@ -25,7 +23,6 @@ open import foundation.inhabited-subtypes open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations -open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels diff --git a/src/real-numbers/similarity-nonnegative-real-numbers.lagda.md b/src/real-numbers/similarity-nonnegative-real-numbers.lagda.md index 3686eb0a01..6b03b09e6f 100644 --- a/src/real-numbers/similarity-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/similarity-nonnegative-real-numbers.lagda.md @@ -7,19 +7,12 @@ module real-numbers.similarity-nonnegative-real-numbers where
Imports ```agda -open import elementary-number-theory.positive-rational-numbers - open import foundation.identity-types -open import foundation.logical-equivalences open import foundation.propositions open import foundation.universe-levels -open import real-numbers.dedekind-real-numbers -open import real-numbers.inequality-real-numbers open import real-numbers.nonnegative-real-numbers -open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers -open import real-numbers.strict-inequality-real-numbers ```
diff --git a/src/real-numbers/similarity-real-numbers.lagda.md b/src/real-numbers/similarity-real-numbers.lagda.md index 5664b3a49b..2c959f7d46 100644 --- a/src/real-numbers/similarity-real-numbers.lagda.md +++ b/src/real-numbers/similarity-real-numbers.lagda.md @@ -7,26 +7,17 @@ module real-numbers.similarity-real-numbers where
Imports ```agda -open import elementary-number-theory.strict-inequality-rational-numbers - -open import foundation.complements-subtypes open import foundation.dependent-pair-types -open import foundation.disjunction -open import foundation.empty-types -open import foundation.function-types open import foundation.identity-types open import foundation.large-equivalence-relations open import foundation.large-similarity-relations open import foundation.logical-equivalences -open import foundation.powersets open import foundation.propositions open import foundation.similarity-subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import order-theory.large-posets open import order-theory.large-preorders -open import order-theory.similarity-of-elements-large-posets open import real-numbers.dedekind-real-numbers ``` diff --git a/src/real-numbers/squares-real-numbers.lagda.md b/src/real-numbers/squares-real-numbers.lagda.md index e9995706b5..86d106d8c6 100644 --- a/src/real-numbers/squares-real-numbers.lagda.md +++ b/src/real-numbers/squares-real-numbers.lagda.md @@ -9,30 +9,23 @@ module real-numbers.squares-real-numbers where
Imports ```agda -open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.intersections-closed-intervals-rational-numbers open import elementary-number-theory.maximum-rational-numbers open import elementary-number-theory.multiplication-closed-intervals-rational-numbers open import elementary-number-theory.multiplication-negative-rational-numbers -open import elementary-number-theory.multiplication-positive-and-negative-rational-numbers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers -open import elementary-number-theory.nonpositive-rational-numbers -open import elementary-number-theory.positive-and-negative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.squares-rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers -open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.disjunction -open import foundation.empty-types open import foundation.existential-quantification -open import foundation.function-types open import foundation.identity-types open import foundation.propositional-truncations open import foundation.transport-along-identifications diff --git a/src/real-numbers/strict-inequalities-addition-and-subtraction-real-numbers.lagda.md b/src/real-numbers/strict-inequalities-addition-and-subtraction-real-numbers.lagda.md index 26b7ac1b7d..20fe2fbe23 100644 --- a/src/real-numbers/strict-inequalities-addition-and-subtraction-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequalities-addition-and-subtraction-real-numbers.lagda.md @@ -21,7 +21,6 @@ open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.dependent-pair-types -open import foundation.empty-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.logical-equivalences @@ -34,7 +33,6 @@ open import real-numbers.addition-real-numbers open import real-numbers.arithmetically-located-dedekind-cuts 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.negation-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.strict-inequality-real-numbers diff --git a/src/real-numbers/strict-inequality-nonnegative-real-numbers.lagda.md b/src/real-numbers/strict-inequality-nonnegative-real-numbers.lagda.md index 07f144ab5d..af7f51e493 100644 --- a/src/real-numbers/strict-inequality-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequality-nonnegative-real-numbers.lagda.md @@ -22,7 +22,6 @@ open import foundation.universe-levels open import logic.functoriality-existential-quantification -open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.nonnegative-real-numbers diff --git a/src/real-numbers/strict-inequality-positive-real-numbers.lagda.md b/src/real-numbers/strict-inequality-positive-real-numbers.lagda.md index a0b7199f32..e24b886aea 100644 --- a/src/real-numbers/strict-inequality-positive-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequality-positive-real-numbers.lagda.md @@ -12,7 +12,6 @@ module real-numbers.strict-inequality-positive-real-numbers where open import foundation.propositions open import foundation.universe-levels -open import real-numbers.dedekind-real-numbers open import real-numbers.positive-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers/strict-inequality-real-numbers.lagda.md b/src/real-numbers/strict-inequality-real-numbers.lagda.md index 96296b0ca7..d632b09a54 100644 --- a/src/real-numbers/strict-inequality-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequality-real-numbers.lagda.md @@ -26,7 +26,6 @@ open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions -open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.universe-levels diff --git a/src/real-numbers/subsets-real-numbers.lagda.md b/src/real-numbers/subsets-real-numbers.lagda.md index b83bc66f44..c42f82f45e 100644 --- a/src/real-numbers/subsets-real-numbers.lagda.md +++ b/src/real-numbers/subsets-real-numbers.lagda.md @@ -20,11 +20,8 @@ open import foundation.involutions open import foundation.logical-equivalences open import foundation.sets 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.equality-of-metric-spaces open import metric-spaces.images-isometries-metric-spaces open import metric-spaces.isometries-metric-spaces diff --git a/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md b/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md index 3f060650bf..02cfcd06db 100644 --- a/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md +++ b/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md @@ -9,8 +9,6 @@ module real-numbers.totally-bounded-subsets-real-numbers where
Imports ```agda -open import elementary-number-theory.positive-rational-numbers - open import foundation.dependent-pair-types open import foundation.propositions open import foundation.subtypes @@ -21,7 +19,6 @@ open import metric-spaces.metric-spaces open import metric-spaces.subspaces-metric-spaces open import metric-spaces.totally-bounded-metric-spaces -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.subsets-real-numbers diff --git a/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md b/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md index 82a733d139..7c96ab1c56 100644 --- a/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/transposition-addition-subtraction-cuts-dedekind-real-numbers.lagda.md @@ -23,7 +23,6 @@ open import real-numbers.dedekind-real-numbers open import real-numbers.difference-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-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers ``` diff --git a/src/real-numbers/upper-dedekind-real-numbers.lagda.md b/src/real-numbers/upper-dedekind-real-numbers.lagda.md index 133ba99ea0..b9ed0136c8 100644 --- a/src/real-numbers/upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/upper-dedekind-real-numbers.lagda.md @@ -24,7 +24,6 @@ open import foundation.existential-quantification open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences -open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.similarity-subtypes From f11b6e2ecc5abdd4eae20346a460807ea293f811 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 9 Nov 2025 13:09:19 +0100 Subject: [PATCH 20/21] fix --- .../multiplicative-inverses-nonzero-real-numbers.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md index ad287640f8..51ab87da43 100644 --- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md @@ -132,8 +132,8 @@ module _ ### If a real number has a multiplicative inverse, it is nonzero ```agda -opaque - unfolding leq-ℝ mul-ℝ real-ℚ sim-ℝ +abstract opaque + unfolding mul-ℝ real-ℚ sim-ℝ is-nonzero-has-right-inverse-mul-ℝ : {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → sim-ℝ (x *ℝ y) one-ℝ → From 2c0bdbcfc81c2e2f20941257b3fbfdec7d3dbdac Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 9 Nov 2025 13:30:32 +0100 Subject: [PATCH 21/21] chore: optimize imports rational numbers --- .../addition-rational-numbers.lagda.md | 1 - .../difference-rational-numbers.lagda.md | 1 - .../distance-rational-numbers.lagda.md | 2 -- .../geometric-sequences-rational-numbers.lagda.md | 4 ---- .../inequality-positive-rational-numbers.lagda.md | 1 - .../metric-additive-group-of-rational-numbers.lagda.md | 2 -- .../multiplicative-group-of-rational-numbers.lagda.md | 2 -- .../negative-rational-numbers.lagda.md | 2 -- .../positive-and-negative-rational-numbers.lagda.md | 2 -- .../positive-rational-numbers.lagda.md | 4 ---- .../powers-nonnegative-rational-numbers.lagda.md | 2 -- .../powers-positive-rational-numbers.lagda.md | 1 - .../powers-rational-numbers.lagda.md | 2 -- .../square-roots-positive-rational-numbers.lagda.md | 1 - .../squares-rational-numbers.lagda.md | 2 -- .../strict-inequality-rational-numbers.lagda.md | 5 ----- src/elementary-number-theory/triangular-numbers.lagda.md | 4 ---- 17 files changed, 38 deletions(-) diff --git a/src/elementary-number-theory/addition-rational-numbers.lagda.md b/src/elementary-number-theory/addition-rational-numbers.lagda.md index 4e3854dddf..72024841c0 100644 --- a/src/elementary-number-theory/addition-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-rational-numbers.lagda.md @@ -23,7 +23,6 @@ open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types -open import foundation.injective-maps open import foundation.interchange-law open import foundation.retractions open import foundation.sections diff --git a/src/elementary-number-theory/difference-rational-numbers.lagda.md b/src/elementary-number-theory/difference-rational-numbers.lagda.md index e4830f7cff..cc782a4c7c 100644 --- a/src/elementary-number-theory/difference-rational-numbers.lagda.md +++ b/src/elementary-number-theory/difference-rational-numbers.lagda.md @@ -17,7 +17,6 @@ open import elementary-number-theory.rational-numbers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.identity-types -open import foundation.interchange-law ```
diff --git a/src/elementary-number-theory/distance-rational-numbers.lagda.md b/src/elementary-number-theory/distance-rational-numbers.lagda.md index 3926d248dc..ccc7b5f8b3 100644 --- a/src/elementary-number-theory/distance-rational-numbers.lagda.md +++ b/src/elementary-number-theory/distance-rational-numbers.lagda.md @@ -21,13 +21,11 @@ open import elementary-number-theory.minimum-rational-numbers open import elementary-number-theory.multiplication-nonnegative-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.nonnegative-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.action-on-identifications-binary-functions 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.function-types diff --git a/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md index 21695e9d15..07004973a8 100644 --- a/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md +++ b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md @@ -29,9 +29,7 @@ open import elementary-number-theory.rational-numbers open import elementary-number-theory.ring-of-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.dependent-pair-types open import foundation.function-extensionality open import foundation.identity-types open import foundation.negated-equality @@ -45,8 +43,6 @@ open import lists.sequences open import metric-spaces.limits-of-sequences-metric-spaces open import metric-spaces.metric-space-of-rational-numbers open import metric-spaces.uniformly-continuous-functions-metric-spaces - -open import order-theory.strictly-increasing-sequences-strictly-preordered-sets ```
diff --git a/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md index 1398ef233b..bd42b31bd9 100644 --- a/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md @@ -13,7 +13,6 @@ open import elementary-number-theory.positive-rational-numbers open import foundation.action-on-identifications-functions open import foundation.binary-relations -open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.universe-levels diff --git a/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md index ba29b98878..c692847c8c 100644 --- a/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md @@ -9,9 +9,7 @@ module elementary-number-theory.metric-additive-group-of-rational-numbers where ```agda open import analysis.metric-abelian-groups -open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers -open import elementary-number-theory.rational-numbers open import foundation.dependent-pair-types open import foundation.universe-levels diff --git a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md index 30f54cea5a..9b527c5f53 100644 --- a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md @@ -16,7 +16,6 @@ open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.multiplicative-monoid-of-rational-numbers open import elementary-number-theory.negative-rational-numbers -open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-rational-numbers open import elementary-number-theory.positive-rational-numbers @@ -27,7 +26,6 @@ open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.dependent-pair-types -open import foundation.empty-types open import foundation.function-types open import foundation.identity-types open import foundation.negated-equality diff --git a/src/elementary-number-theory/negative-rational-numbers.lagda.md b/src/elementary-number-theory/negative-rational-numbers.lagda.md index 7a41b1a752..15c00ecac4 100644 --- a/src/elementary-number-theory/negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/negative-rational-numbers.lagda.md @@ -17,13 +17,11 @@ open import elementary-number-theory.negative-integer-fractions open import elementary-number-theory.negative-integers open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-integers -open import elementary-number-theory.positive-integer-fractions open import elementary-number-theory.positive-integers 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.action-on-identifications-functions open import foundation.binary-relations open import foundation.binary-transport open import foundation.dependent-pair-types diff --git a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md index 021ef28f50..09a711a99e 100644 --- a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md @@ -11,13 +11,11 @@ open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.nonpositive-rational-numbers -open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-integers 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.binary-transport open import foundation.cartesian-product-types open import foundation.coproduct-types open import foundation.dependent-pair-types diff --git a/src/elementary-number-theory/positive-rational-numbers.lagda.md b/src/elementary-number-theory/positive-rational-numbers.lagda.md index f146b5f15f..eda656f821 100644 --- a/src/elementary-number-theory/positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-rational-numbers.lagda.md @@ -15,17 +15,13 @@ open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers -open import elementary-number-theory.negative-integers open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.nonzero-rational-numbers -open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-integer-fractions open import elementary-number-theory.positive-integers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers -open import foundation.cartesian-product-types -open import foundation.coproduct-types open import foundation.decidable-propositions open import foundation.decidable-subtypes open import foundation.dependent-pair-types diff --git a/src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md index 535de72152..b07d9baf6d 100644 --- a/src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md @@ -17,7 +17,6 @@ open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplicative-monoid-of-nonnegative-rational-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonnegative-rational-numbers -open import elementary-number-theory.positive-and-negative-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-nonnegative-rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers @@ -27,7 +26,6 @@ open import foundation.empty-types open import foundation.identity-types open import group-theory.powers-of-elements-commutative-monoids -open import group-theory.powers-of-elements-monoids ```
diff --git a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md index 05641432b4..1e1dbbcd56 100644 --- a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md @@ -25,7 +25,6 @@ open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonnegative-rational-numbers -open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.positive-and-negative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers diff --git a/src/elementary-number-theory/powers-rational-numbers.lagda.md b/src/elementary-number-theory/powers-rational-numbers.lagda.md index ea1efba98d..51e308477d 100644 --- a/src/elementary-number-theory/powers-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-rational-numbers.lagda.md @@ -14,9 +14,7 @@ open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.inequality-nonnegative-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.multiplication-natural-numbers -open import elementary-number-theory.multiplication-nonnegative-rational-numbers open import elementary-number-theory.multiplication-positive-and-negative-rational-numbers -open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.multiplicative-monoid-of-rational-numbers open import elementary-number-theory.natural-numbers diff --git a/src/elementary-number-theory/square-roots-positive-rational-numbers.lagda.md b/src/elementary-number-theory/square-roots-positive-rational-numbers.lagda.md index 7687c6d3d4..c6621bc79b 100644 --- a/src/elementary-number-theory/square-roots-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/square-roots-positive-rational-numbers.lagda.md @@ -14,7 +14,6 @@ open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequality-rational-numbers -open import elementary-number-theory.maximum-rational-numbers open import elementary-number-theory.minimum-positive-rational-numbers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers diff --git a/src/elementary-number-theory/squares-rational-numbers.lagda.md b/src/elementary-number-theory/squares-rational-numbers.lagda.md index ada7062ba5..41b169790a 100644 --- a/src/elementary-number-theory/squares-rational-numbers.lagda.md +++ b/src/elementary-number-theory/squares-rational-numbers.lagda.md @@ -18,7 +18,6 @@ open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.maximum-rational-numbers open import elementary-number-theory.multiplication-negative-rational-numbers open import elementary-number-theory.multiplication-nonnegative-rational-numbers -open import elementary-number-theory.multiplication-nonpositive-rational-numbers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.negative-rational-numbers @@ -31,7 +30,6 @@ open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions open import foundation.coproduct-types -open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.function-types diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index ddaa7ba616..e237a00ca0 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -13,10 +13,7 @@ open import elementary-number-theory.addition-integer-fractions open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.cross-multiplication-difference-integer-fractions -open import elementary-number-theory.difference-integers open import elementary-number-theory.difference-rational-numbers -open import elementary-number-theory.inequality-integer-fractions -open import elementary-number-theory.inequality-integers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers @@ -26,7 +23,6 @@ open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonnegative-integers open import elementary-number-theory.nonpositive-integers open import elementary-number-theory.positive-and-negative-integers -open import elementary-number-theory.positive-integers open import elementary-number-theory.rational-numbers open import elementary-number-theory.reduced-integer-fractions open import elementary-number-theory.strict-inequality-integer-fractions @@ -36,7 +32,6 @@ open import elementary-number-theory.strict-inequality-natural-numbers open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.binary-transport -open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.coproduct-types open import foundation.decidable-propositions diff --git a/src/elementary-number-theory/triangular-numbers.lagda.md b/src/elementary-number-theory/triangular-numbers.lagda.md index 451206ca03..23ae32125c 100644 --- a/src/elementary-number-theory/triangular-numbers.lagda.md +++ b/src/elementary-number-theory/triangular-numbers.lagda.md @@ -35,20 +35,16 @@ open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.homotopies open import foundation.identity-types -open import foundation.transport-along-identifications open import group-theory.abelian-groups open import group-theory.groups -open import lists.sequences - open import metric-spaces.limits-of-sequences-metric-spaces open import metric-spaces.metric-space-of-rational-numbers open import metric-spaces.rational-sequences-approximating-zero open import metric-spaces.uniformly-continuous-functions-metric-spaces open import ring-theory.partial-sums-sequences-semirings -open import ring-theory.sums-of-finite-sequences-of-elements-semirings ```