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 3a42ec9a40..657fd42d16 100644 --- a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md +++ b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md @@ -177,7 +177,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..78b872ffe9 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-ℚ⁺ = @@ -334,23 +334,16 @@ module _ ((d : ℚ⁺) → leq-ℚ x (y +ℚ (rational-ℚ⁺ d))) → leq-ℚ x y leq-leq-add-positive-ℚ H = rec-coproduct - ( λ I → + ( λ y diff --git a/src/elementary-number-theory/distance-rational-numbers.lagda.md b/src/elementary-number-theory/distance-rational-numbers.lagda.md index 6a9bcc3d5d..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 @@ -191,10 +189,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/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/inequalities-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md index 88ac145a32..8d8b52b30f 100644 --- a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md @@ -101,8 +101,8 @@ abstract ```agda abstract is-positive-le-ℚ⁰⁺ : - (p : ℚ⁰⁺) (q : ℚ) → le-ℚ (rational-ℚ⁰⁺ p) q → is-positive-ℚ q - is-positive-le-ℚ⁰⁺ (p , nonneg-p) q p +ℚ 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-interior-closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-interior-closed-intervals-rational-numbers.lagda.md index b05bb91cc0..ed0f43ca73 100644 --- a/src/elementary-number-theory/multiplication-interior-closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-interior-closed-intervals-rational-numbers.lagda.md @@ -1,6 +1,8 @@ # Multiplication of interior intervals of closed intervals of rational numbers ```agda +{-# OPTIONS --lossy-unification #-} + module elementary-number-theory.multiplication-interior-closed-intervals-rational-numbers where ``` @@ -325,12 +327,10 @@ abstract ( a' @@ -122,7 +120,7 @@ abstract ( power-ℚ⁰⁺ (succ-ℕ n) q) ( preserves-leq-left-mul-ℚ⁰⁺ (power-ℚ⁰⁺ n p) _ _ (leq-le-ℚ p diff --git a/src/metric-spaces/located-metric-spaces.lagda.md b/src/metric-spaces/located-metric-spaces.lagda.md index 1fef763229..a5d4416fc0 100644 --- a/src/metric-spaces/located-metric-spaces.lagda.md +++ b/src/metric-spaces/located-metric-spaces.lagda.md @@ -137,8 +137,7 @@ module _ let r = mediant-ℚ p q p⁺ = (p , is-positive-le-zero-ℚ 0Imports + +```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-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-and-subtraction-real-numbers +open import real-numbers.strict-inequality-nonnegative-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-real-numbers.lagda.md b/src/real-numbers/addition-real-numbers.lagda.md index 70d1e41be9..8f67041ac9 100644 --- a/src/real-numbers/addition-real-numbers.lagda.md +++ b/src/real-numbers/addition-real-numbers.lagda.md @@ -11,8 +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.additive-group-of-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 @@ -20,10 +18,8 @@ open import foundation.action-on-identifications-binary-functions 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.empty-types -open import foundation.equivalences open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-cartesian-product-types @@ -33,12 +29,6 @@ open import foundation.propositional-truncations 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.monoids -open import group-theory.semigroups - open import logic.functoriality-existential-quantification open import real-numbers.addition-lower-dedekind-real-numbers @@ -46,7 +36,6 @@ open import real-numbers.addition-upper-dedekind-real-numbers open import real-numbers.arithmetically-located-dedekind-cuts 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.negation-real-numbers open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers @@ -98,8 +87,8 @@ module _ { qx} { py} { qy} - ( le-lower-upper-cut-ℝ x px qx pxImports ```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 af40140487..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 @@ -204,7 +202,7 @@ module _ ( preserves-leq-left-add-ℚ (q -ℚ p) p' p p'≤p))) ( q'∈U))) ( decide-le-leq-ℚ p p')) - ( arithmetically-located (positive-diff-le-ℚ p q 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 foundation.action-on-identifications-functions open import foundation.dependent-pair-types @@ -28,6 +26,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-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 @@ -82,11 +81,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-ℝ : @@ -124,8 +125,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)) @@ -138,19 +137,17 @@ abstract lower-neighborhood-ℝ d y x lower-neighborhood-diff-ℝ d⁺@(d , _) x y x-y≤d q q+dImports + +```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 + + abstract 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-ℝ + ( 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-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md index 5f31c60805..7e9c14d77b 100644 --- a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md @@ -18,8 +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.negation -open import foundation.powersets open import foundation.propositions open import foundation.subtypes open import foundation.unit-type 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..dc71c190c0 --- /dev/null +++ b/src/real-numbers/inequality-nonnegative-real-numbers.lagda.md @@ -0,0 +1,158 @@ +# 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.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 @@ -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 @@ -139,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 @@ -187,26 +175,26 @@ module _ ### Inequality on the real numbers is reflexive ```agda -opaque +abstract opaque unfolding leq-ℝ refl-leq-ℝ : {l : Level} (x : ℝ l) → leq-ℝ x x refl-leq-ℝ x = refl-leq-Large-Preorder lower-ℝ-Large-Preorder (lower-real-ℝ x) - leq-eq-ℝ : {l : Level} (x y : ℝ l) → x = y → leq-ℝ x y - leq-eq-ℝ x y x=y = tr (leq-ℝ x) x=y (refl-leq-ℝ x) + 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 - leq-sim-ℝ _ _ = pr1 + leq-sim-ℝ : {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → sim-ℝ x y → leq-ℝ x y + leq-sim-ℝ = pr1 ``` ### Inequality on the real numbers is antisymmetric ```agda -opaque +abstract opaque unfolding leq-ℝ sim-ℝ sim-antisymmetric-leq-ℝ : @@ -227,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 @@ -256,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-ℝ : @@ -288,27 +276,31 @@ opaque ### The canonical map from rational numbers to the reals preserves and reflects inequality ```agda -opaque - unfolding leq-ℝ real-ℚ +module _ + {x y : ℚ} + where - preserves-leq-real-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℝ (real-ℚ x) (real-ℚ y) - preserves-leq-real-ℚ = preserves-leq-lower-real-ℚ + abstract opaque + unfolding leq-ℝ real-ℚ - reflects-leq-real-ℚ : (x y : ℚ) → leq-ℝ (real-ℚ x) (real-ℚ y) → leq-ℚ x y - reflects-leq-real-ℚ = reflects-leq-lower-real-ℚ + preserves-leq-real-ℚ : leq-ℚ x y → leq-ℝ (real-ℚ x) (real-ℚ y) + preserves-leq-real-ℚ = preserves-leq-lower-real-ℚ x y - iff-leq-real-ℚ : (x y : ℚ) → leq-ℚ x y ↔ leq-ℝ (real-ℚ x) (real-ℚ y) - iff-leq-real-ℚ = iff-leq-lower-real-ℚ + reflects-leq-real-ℚ : leq-ℝ (real-ℚ x) (real-ℚ y) → leq-ℚ x y + reflects-leq-real-ℚ = reflects-leq-lower-real-ℚ x y + + iff-leq-real-ℚ : leq-ℚ x y ↔ leq-ℝ (real-ℚ x) (real-ℚ y) + iff-leq-real-ℚ = iff-leq-lower-real-ℚ x y ``` ### Negation reverses inequality on the real numbers ```agda module _ - {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) + {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) @@ -319,10 +311,10 @@ module _ ```agda module _ - {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) (x~y : sim-ℝ x y) + {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 @@ -333,248 +325,15 @@ 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 preserves-leq-sim-ℝ : leq-ℝ x1 y1 → leq-ℝ x2 y2 preserves-leq-sim-ℝ x1≤y1 = preserves-leq-left-sim-ℝ - ( y2) - ( x1) - ( x2) ( x1~x2) - ( preserves-leq-right-sim-ℝ x1 y1 y2 y1~y2 x1≤y1) -``` - -### 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 b c 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-ℝ - ( z +ℝ y) - ( (x -ℝ y) +ℝ y) - ( x) - ( 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-ℝ - (z -ℝ y) - ( (x +ℝ y) -ℝ y) - ( x) - ( 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-ℝ - ( x -ℝ z) - ( (y +ℝ z) -ℝ z) - ( y) - ( 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-ℝ - ( x +ℝ z) - ( (y -ℝ z) +ℝ z) - ( y) - ( 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)) -``` - -### 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-ℝ - ( x -ℝ real-ℚ⁺ d) - ( y) - ( leq-transpose-right-add-ℝ - ( x) - ( y) - ( real-ℚ⁺ d) - ( x≤y+d))) + ( preserves-leq-right-sim-ℝ y1~y2 x1≤y1) ``` ### `x ≤ q` for a rational `q` if and only if `q ∉ lower-cut-ℝ x` @@ -584,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) @@ -617,7 +376,7 @@ module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where - opaque + abstract opaque unfolding leq-ℝ' leq-leq-rational-ℝ : 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/infima-families-real-numbers.lagda.md b/src/real-numbers/infima-families-real-numbers.lagda.md index 6b3be4283a..0b338cbe37 100644 --- a/src/real-numbers/infima-families-real-numbers.lagda.md +++ b/src/real-numbers/infima-families-real-numbers.lagda.md @@ -41,6 +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-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 @@ -149,7 +150,7 @@ module _ not-leq-le-ℝ (y i) z ( transitive-le-ℝ (y i) (x +ℝ real-ℚ ε) z ( le-transpose-right-diff-ℝ' _ z _ - ( le-real-is-in-lower-cut-ℚ ε (z -ℝ x) ε diff --git a/src/real-numbers/isometry-negation-real-numbers.lagda.md b/src/real-numbers/isometry-negation-real-numbers.lagda.md index 8854080f8e..3c2b449432 100644 --- a/src/real-numbers/isometry-negation-real-numbers.lagda.md +++ b/src/real-numbers/isometry-negation-real-numbers.lagda.md @@ -11,19 +11,23 @@ module real-numbers.isometry-negation-real-numbers where ```agda open import elementary-number-theory.positive-rational-numbers +open import foundation.action-on-identifications-functions open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types +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 +open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.metric-space-of-real-numbers open import real-numbers.negation-real-numbers +open import real-numbers.rational-real-numbers ``` @@ -36,6 +40,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/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 9e1a1f4786..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,13 +24,12 @@ 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 open import real-numbers.metric-space-of-real-numbers @@ -90,7 +85,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 +93,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..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,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-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-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers ``` @@ -130,10 +132,7 @@ module _ diagonal-product ( (r : ℚ) → is-in-lower-cut-ℝ x (r +ℚ (rational-ℚ⁺ d)) → is-in-lower-cut-ℝ x r) - ( λ r → - le-lower-cut-ℝ x r - ( r +ℚ rational-ℚ⁺ d) - ( le-right-add-rational-ℚ⁺ r d)) + ( λ r → le-lower-cut-ℝ x (le-right-add-rational-ℚ⁺ r d)) is-symmetric-neighborhood-ℝ : is-symmetric-Rational-Neighborhood-Relation (neighborhood-prop-ℝ l) @@ -170,15 +169,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 +216,11 @@ module _ ( lower-cut-ℝ y r) ( λ s (r 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-negative-real-numbers.lagda.md b/src/real-numbers/multiplication-negative-real-numbers.lagda.md index af8ae9cbfa..7d2e4c8289 100644 --- a/src/real-numbers/multiplication-negative-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-negative-real-numbers.lagda.md @@ -69,14 +69,14 @@ _*ℝ⁻_ = mul-ℝ⁻ ```agda abstract reverses-le-left-mul-ℝ⁻ : - {l1 l2 l3 : Level} (x : ℝ⁻ l1) (y : ℝ l2) (z : ℝ l3) → le-ℝ y z → + {l1 l2 l3 : Level} (x : ℝ⁻ l1) {y : ℝ l2} {z : ℝ l3} → le-ℝ y z → le-ℝ (real-ℝ⁻ x *ℝ z) (real-ℝ⁻ x *ℝ y) - reverses-le-left-mul-ℝ⁻ x y z yImports ```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 @@ -53,7 +52,7 @@ module _ {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} where - opaque + abstract opaque unfolding mul-ℝ is-positive-mul-ℝ : @@ -66,10 +65,10 @@ module _ (c⁺@(c , _) , cImports ```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 ``` @@ -83,7 +70,7 @@ module _ ( disjunction-Prop (lower-cut-neg-ℝ q) (upper-cut-neg-ℝ r)) ( inr-disjunction) ( inl-disjunction) - ( is-located-lower-upper-cut-ℝ x (neg-ℚ r) (neg-ℚ q) (neg-le-ℚ qImports ```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,32 +18,26 @@ 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 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 +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.saturation-inequality-real-numbers -open import real-numbers.similarity-real-numbers open import real-numbers.strict-inequality-real-numbers -open import real-numbers.subsets-real-numbers ``` @@ -101,8 +93,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 ``` @@ -125,12 +121,14 @@ eq-ℝ⁰⁺ _ _ = eq-type-subtype is-nonnegative-prop-ℝ ```agda abstract - is-nonnegative-real-ℚ⁰⁺ : (q : ℚ⁰⁺) → is-nonnegative-ℝ (real-ℚ⁰⁺ q) - is-nonnegative-real-ℚ⁰⁺ (q , nonneg-q) = - preserves-leq-real-ℚ zero-ℚ q (leq-zero-is-nonnegative-ℚ nonneg-q) + preserves-is-nonnegative-real-ℚ : + {q : ℚ} → is-nonnegative-ℚ q → is-nonnegative-ℝ (real-ℚ q) + preserves-is-nonnegative-real-ℚ is-nonneg-q = + preserves-leq-real-ℚ (leq-zero-is-nonnegative-ℚ is-nonneg-q) nonnegative-real-ℚ⁰⁺ : ℚ⁰⁺ → ℝ⁰⁺ lzero -nonnegative-real-ℚ⁰⁺ q = (real-ℚ⁰⁺ q , is-nonnegative-real-ℚ⁰⁺ q) +nonnegative-real-ℚ⁰⁺ (q , is-nonneg-q) = + ( real-ℚ q , preserves-is-nonnegative-real-ℚ is-nonneg-q) nonnegative-real-ℚ⁺ : ℚ⁺ → ℝ⁰⁺ lzero nonnegative-real-ℚ⁺ q = nonnegative-real-ℚ⁰⁺ (nonnegative-ℚ⁺ q) @@ -146,105 +144,22 @@ one-ℝ⁰⁺ : ℝ⁰⁺ lzero one-ℝ⁰⁺ = nonnegative-real-ℚ⁰⁺ one-ℚ⁰⁺ ``` -### 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-ℝ -``` - -### Inequality on nonnegative real numbers - -```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-ℝ⁰⁺ -``` - -### 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-ℝ (real-ℝ⁰⁺ z) _ _ 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) -``` - ### A real number is nonnegative if and only if every element of its upper cut is positive ```agda abstract is-positive-is-in-upper-cut-ℝ⁰⁺ : - {l : Level} → (x : ℝ⁰⁺ l) (q : ℚ) → is-in-upper-cut-ℝ⁰⁺ x q → + {l : Level} → (x : ℝ⁰⁺ l) {q : ℚ} → is-in-upper-cut-ℝ⁰⁺ x q → is-positive-ℚ q - is-positive-is-in-upper-cut-ℝ⁰⁺ (x , 0≤x) q xImports ```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 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-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers ``` @@ -122,7 +114,7 @@ is-rounded-upper-cut-ℝ⁺ : is-rounded-upper-cut-ℝ⁺ (x , _) = is-rounded-upper-cut-ℝ x le-lower-upper-cut-ℝ⁺ : - {l : Level} (x : ℝ⁺ l) (p q : ℚ) → + {l : Level} (x : ℝ⁺ l) {p q : ℚ} → is-in-lower-cut-ℝ⁺ x p → is-in-upper-cut-ℝ⁺ x q → le-ℚ p q le-lower-upper-cut-ℝ⁺ (x , _) = le-lower-upper-cut-ℝ x ``` @@ -144,8 +136,7 @@ module _ abstract is-positive-iff-zero-in-lower-cut-ℝ : is-positive-ℝ x ↔ is-in-lower-cut-ℝ x zero-ℚ - is-positive-iff-zero-in-lower-cut-ℝ = - inv-iff (le-real-iff-lower-cut-ℚ zero-ℚ x) + is-positive-iff-zero-in-lower-cut-ℝ = inv-iff (le-real-iff-lower-cut-ℚ x) is-positive-zero-in-lower-cut-ℝ : is-in-lower-cut-ℝ x zero-ℚ → is-positive-ℝ x @@ -165,7 +156,7 @@ module _ {l : Level} (x : ℝ l) where - opaque + abstract opaque unfolding le-ℝ real-ℚ exists-ℚ⁺-in-lower-cut-is-positive-ℝ : @@ -198,7 +189,7 @@ exists-ℚ⁺-in-lower-cut-ℝ⁺ = ind-Σ exists-ℚ⁺-in-lower-cut-is-positiv ### Addition with a positive real number is a strictly inflationary map ```agda -opaque +abstract opaque unfolding add-ℝ le-ℝ le-left-add-real-ℝ⁺ : @@ -266,24 +257,19 @@ abstract ### The canonical embedding of rational numbers preserves positivity ```agda -preserves-is-positive-real-ℚ : - (q : ℚ) → is-positive-ℚ q → is-positive-ℝ (real-ℚ q) -preserves-is-positive-real-ℚ q pos-q = - preserves-le-real-ℚ zero-ℚ q (le-zero-is-positive-ℚ pos-q) - -opaque - unfolding le-ℝ real-ℚ - - is-positive-rational-is-positive-real-ℚ : - (q : ℚ) → is-positive-ℝ (real-ℚ q) → is-positive-ℚ q - is-positive-rational-is-positive-real-ℚ q = - elim-exists - ( is-positive-prop-ℚ q) - ( λ r (0Imports ```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 ``` @@ -66,12 +55,10 @@ the [image](foundation.images.md) of this embedding ```agda is-dedekind-lower-upper-real-ℚ : (x : ℚ) → - is-dedekind-lower-upper-ℝ - ( lower-real-ℚ x) - ( upper-real-ℚ x) + is-dedekind-lower-upper-ℝ (lower-real-ℚ x) (upper-real-ℚ x) is-dedekind-lower-upper-real-ℚ x = - (λ q (H , K) → asymmetric-le-ℚ q x H K) , - located-le-ℚ x + ( (λ q (H , K) → asymmetric-le-ℚ q x H K) , + located-le-ℚ x) ``` ### The canonical map from `ℚ` to `ℝ lzero` @@ -161,7 +148,7 @@ all-eq-is-rational-ℝ x p q H H' = ( empty-Prop) ( pr1 H) ( pr2 H') - ( is-located-lower-upper-cut-ℝ x p q I)) + ( is-located-lower-upper-cut-ℝ x I)) right-case : le-ℚ q p → p = q right-case I = @@ -170,7 +157,7 @@ all-eq-is-rational-ℝ x p q H H' = ( empty-Prop) ( pr1 H') ( pr2 H) - ( is-located-lower-upper-cut-ℝ x q p I)) + ( is-located-lower-upper-cut-ℝ x I)) is-prop-rational-real : {l : Level} (x : ℝ l) → is-prop (Σ ℚ (is-rational-ℝ x)) is-prop-rational-real x = @@ -234,13 +221,13 @@ opaque ( q) ( id) ( λ p=q → ex-falso (q∉lx (tr (is-in-lower-cut-ℝ x) p=q p∈lx))) - ( λ q

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 @@ -94,8 +91,8 @@ module _ (p , pImports ```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 @@ -41,7 +38,8 @@ open import real-numbers.upper-dedekind-real-numbers Given an [upper Dedekind real number](real-numbers.upper-dedekind-real-numbers.md) `x`, we can convert `x` to a -[Dedekind real number](real-numbers.dedekind-real-numbers.md) if and only if the +[Dedekind real number](real-numbers.dedekind-real-numbers.md) +[if and only if](foundation.logical-equivalences.md) the [complement](foundation.complements-subtypes.md) of the cut of `x` is [inhabited](foundation.inhabited-subtypes.md) and for any `p q : ℚ` with `p < q`, `p` is in the [complement](foundation.complements-subtypes.md) of the @@ -89,8 +87,8 @@ module _ (r , qImports + +```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 this page is dedicated to just this property 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..fad1d8e16c 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-and-subtraction-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.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-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 +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/similarity-nonnegative-real-numbers.lagda.md b/src/real-numbers/similarity-nonnegative-real-numbers.lagda.md new file mode 100644 index 0000000000..6b03b09e6f --- /dev/null +++ b/src/real-numbers/similarity-nonnegative-real-numbers.lagda.md @@ -0,0 +1,63 @@ +# Similarity of nonnegative real numbers + +```agda +module real-numbers.similarity-nonnegative-real-numbers where +``` + +
Imports + +```agda +open import foundation.identity-types +open import foundation.propositions +open import foundation.universe-levels + +open import real-numbers.nonnegative-real-numbers +open import real-numbers.similarity-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/similarity-positive-real-numbers.lagda.md b/src/real-numbers/similarity-positive-real-numbers.lagda.md new file mode 100644 index 0000000000..0dbfb733ac --- /dev/null +++ b/src/real-numbers/similarity-positive-real-numbers.lagda.md @@ -0,0 +1,35 @@ +# Similarity of positive real numbers + +```agda +module real-numbers.similarity-positive-real-numbers where +``` + +
Imports + +```agda +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 +``` + +
+ +## 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/similarity-real-numbers.lagda.md b/src/real-numbers/similarity-real-numbers.lagda.md index 3f8a1ef83c..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 ``` @@ -70,7 +61,7 @@ module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where - opaque + abstract opaque unfolding sim-ℝ sim-lower-cut-iff-sim-ℝ : @@ -85,7 +76,7 @@ module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where - opaque + abstract opaque unfolding sim-ℝ sim-sim-upper-cut-ℝ : sim-subtype (upper-cut-ℝ x) (upper-cut-ℝ y) → (x ~ℝ y) @@ -102,7 +93,7 @@ module _ ### Reflexivity ```agda -opaque +abstract opaque unfolding sim-ℝ refl-sim-ℝ : {l : Level} → (x : ℝ l) → x ~ℝ x @@ -115,7 +106,7 @@ opaque ### Symmetry ```agda -opaque +abstract opaque unfolding sim-ℝ symmetric-sim-ℝ : @@ -127,7 +118,7 @@ opaque ### Transitivity ```agda -opaque +abstract opaque unfolding sim-ℝ transitive-sim-ℝ : @@ -141,7 +132,7 @@ opaque ### Similar real numbers in the same universe are equal ```agda -opaque +abstract opaque unfolding sim-ℝ eq-sim-ℝ : {l : Level} → {x y : ℝ l} → x ~ℝ y → x = y @@ -185,7 +176,7 @@ similarity-reasoning-ℝ infixl 1 similarity-reasoning-ℝ_ infixl 0 step-similarity-reasoning-ℝ -opaque +abstract opaque unfolding sim-ℝ similarity-reasoning-ℝ_ : 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..d73dc98a0f 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 ``` @@ -104,7 +105,7 @@ module _ (p⁺@(p , is-pos-p) , qImports ```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 @@ -74,7 +67,7 @@ square-ℝ x = x *ℝ x ### The square of a real number is nonnegative ```agda -opaque +abstract opaque unfolding mul-ℝ is-nonnegative-square-ℝ : @@ -123,7 +116,6 @@ opaque in is-positive-le-ℚ⁺ ( a'⁻ *ℚ⁻ a'⁻) - ( q) ( concatenate-leq-le-ℚ ( a' *ℚ a') ( upper-bound-mul-closed-interval-ℚ [a',b'] [a',b']) @@ -138,7 +130,6 @@ opaque in is-positive-le-ℚ⁺ ( b'⁺ *ℚ⁺ b'⁺) - ( q) ( concatenate-leq-le-ℚ ( b' *ℚ b') ( upper-bound-mul-closed-interval-ℚ [a',b'] [a',b']) @@ -148,7 +139,7 @@ opaque ( leq-right-max-ℚ _ _)) ( [a',b'][a',b']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.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.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.negation-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +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 +[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 + + abstract opaque + unfolding add-ℝ le-ℝ + + preserves-le-right-add-ℝ : le-ℝ x y → le-ℝ (x +ℝ z) (y +ℝ z) + preserves-le-right-add-ℝ xImports ```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,18 @@ 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,50 +66,38 @@ le-prop-ℝ x y = (le-ℝ x y , is-prop-le-ℝ x y) ### Strict inequality on the reals implies inequality ```agda -module _ - {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) - where - - opaque - unfolding le-ℝ leq-ℝ - - leq-le-ℝ : le-ℝ x y → leq-ℝ x y - leq-le-ℝ xImports ```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 ac543613a6..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,7 @@ 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 ``` @@ -56,7 +56,6 @@ module _ is-in-lower-cut-ℝ (x -ℝ real-ℚ q) p transpose-add-is-in-lower-cut-ℝ p+q