diff --git a/.vscode/agda.code-snippets b/.vscode/agda.code-snippets index 817c4485b28..8b9bd16ade6 100644 --- a/.vscode/agda.code-snippets +++ b/.vscode/agda.code-snippets @@ -35,5 +35,10 @@ "body": ["retract-reasoning ? retract-of ? by ?"], "description": "Retract reasoning", "prefix": ["retract-reasoning"] + }, + "Inequality reasoning": { + "body": ["chain-of-inequalities ? ≤ ? by ?"], + "description": "Inequality reasoning", + "prefix": ["chain-of-inequalities"] } } 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 fd1909ddece..723cfd0b4c7 100644 --- a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md @@ -12,6 +12,7 @@ module elementary-number-theory.addition-positive-rational-numbers where 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-positive-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.minimum-positive-rational-numbers open import elementary-number-theory.positive-integer-fractions @@ -131,6 +132,37 @@ interchange-law-add-add-ℚ⁺ x y u v = ( rational-ℚ⁺ v)) ``` +### Addition with a positive rational number is a strictly increasing map + +```agda +abstract + le-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x ((rational-ℚ⁺ d) +ℚ x) + le-left-add-rational-ℚ⁺ x d = + concatenate-leq-le-ℚ + ( x) + ( zero-ℚ +ℚ x) + ( (rational-ℚ⁺ d) +ℚ x) + ( inv-tr (leq-ℚ x) (left-unit-law-add-ℚ x) (refl-leq-ℚ x)) + ( preserves-le-left-add-ℚ + ( x) + ( zero-ℚ) + ( rational-ℚ⁺ d) + ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ d))) + + le-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x (x +ℚ (rational-ℚ⁺ d)) + le-right-add-rational-ℚ⁺ x d = + inv-tr + ( le-ℚ x) + ( commutative-add-ℚ x (rational-ℚ⁺ d)) + ( le-left-add-rational-ℚ⁺ x d) + + leq-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (rational-ℚ⁺ d +ℚ x) + leq-left-add-rational-ℚ⁺ x d = leq-le-ℚ (le-left-add-rational-ℚ⁺ x d) + + leq-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (x +ℚ rational-ℚ⁺ d) + leq-right-add-rational-ℚ⁺ x d = leq-le-ℚ (le-right-add-rational-ℚ⁺ x d) +``` + ### The sum of two positive rational numbers is greater than each of them ```agda @@ -138,27 +170,13 @@ module _ (x y : ℚ⁺) where - le-left-add-ℚ⁺ : le-ℚ⁺ x (x +ℚ⁺ y) - le-left-add-ℚ⁺ = - tr - ( λ z → le-ℚ z ((rational-ℚ⁺ x) +ℚ (rational-ℚ⁺ y))) - ( right-unit-law-add-ℚ (rational-ℚ⁺ x)) - ( preserves-le-right-add-ℚ - ( rational-ℚ⁺ x) - ( zero-ℚ) - ( rational-ℚ⁺ y) - ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ y))) - - le-right-add-ℚ⁺ : le-ℚ⁺ y (x +ℚ⁺ y) + le-right-add-ℚ⁺ : le-ℚ⁺ x (x +ℚ⁺ y) le-right-add-ℚ⁺ = - tr - ( λ z → le-ℚ z ((rational-ℚ⁺ x) +ℚ (rational-ℚ⁺ y))) - ( left-unit-law-add-ℚ (rational-ℚ⁺ y)) - ( preserves-le-left-add-ℚ - ( rational-ℚ⁺ y) - ( zero-ℚ) - ( rational-ℚ⁺ x) - ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ x))) + le-right-add-rational-ℚ⁺ (rational-ℚ⁺ x) y + + le-left-add-ℚ⁺ : le-ℚ⁺ y (x +ℚ⁺ y) + le-left-add-ℚ⁺ = + le-left-add-rational-ℚ⁺ (rational-ℚ⁺ y) x ``` ### The positive difference of strictly inequal positive rational numbers @@ -196,7 +214,7 @@ module _ tr ( le-ℚ⁺ le-diff-ℚ⁺) ( left-diff-law-add-ℚ⁺) - ( le-left-add-ℚ⁺ le-diff-ℚ⁺ x) + ( le-right-add-ℚ⁺ le-diff-ℚ⁺ x) ``` ### Any positive rational number can be expressed as the sum of two positive rational numbers @@ -229,12 +247,18 @@ module _ le-left-summand-split-ℚ⁺ : le-ℚ⁺ left-summand-split-ℚ⁺ x le-left-summand-split-ℚ⁺ = le-mediant-zero-ℚ⁺ x + leq-left-summand-split-ℚ⁺ : leq-ℚ⁺ left-summand-split-ℚ⁺ x + leq-left-summand-split-ℚ⁺ = leq-le-ℚ le-left-summand-split-ℚ⁺ + le-right-summand-split-ℚ⁺ : le-ℚ⁺ right-summand-split-ℚ⁺ x le-right-summand-split-ℚ⁺ = tr ( le-ℚ⁺ right-summand-split-ℚ⁺) ( eq-add-split-ℚ⁺) - ( le-right-add-ℚ⁺ left-summand-split-ℚ⁺ right-summand-split-ℚ⁺) + ( le-left-add-ℚ⁺ left-summand-split-ℚ⁺ right-summand-split-ℚ⁺) + + leq-right-summand-split-ℚ⁺ : leq-ℚ⁺ right-summand-split-ℚ⁺ x + leq-right-summand-split-ℚ⁺ = leq-le-ℚ le-right-summand-split-ℚ⁺ le-add-split-ℚ⁺ : (p q r s : ℚ) → @@ -259,37 +283,6 @@ module _ ( rImports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.axiom-of-countable-choice +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.universe-levels + +open import metric-spaces.functions-metric-spaces +open import metric-spaces.limits-of-functions-metric-spaces +open import metric-spaces.metric-spaces +``` + + + +## Idea + +The +{{#concept "classical definition of a limit" WDID=Q1042034 WD="(ε, δ)-definition of limit" Disambiguation="in a metric space" Agda=is-classical-limit-map-Metric-Space}} +states that the limit of `f x` as `x` approaches `x₀` is a `y` such that for any +`ε : ℚ⁺`, there [exists](foundation.existential-quantification.md) a `δ : ℚ⁺` +such that if `x` and `x₀` are in a `δ`-neighborhood of each other, `f x` and `y` +are in a `ε`-neighborhood of each other. + +The constructive definition implies the classical definition, but the other +direction requires the +[axiom of countable choice](foundation.axiom-of-countable-choice.md). + +## Definition + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + (x : type-Metric-Space X) + (y : type-Metric-Space Y) + where + + is-classical-limit-prop-map-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4) + is-classical-limit-prop-map-Metric-Space = + Π-Prop + ( ℚ⁺) + ( λ ε → + ∃ ( ℚ⁺) + ( λ δ → + Π-Prop + ( type-Metric-Space X) + ( λ x' → + neighborhood-prop-Metric-Space X δ x x' ⇒ + neighborhood-prop-Metric-Space Y ε y (f x')))) + + is-classical-limit-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) + is-classical-limit-map-Metric-Space = + type-Prop is-classical-limit-prop-map-Metric-Space +``` + +## Properties + +### Constructive limits are classical limits + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + (x : type-Metric-Space X) + (y : type-Metric-Space Y) + where + + abstract + is-classical-limit-is-limit-map-Metric-Space : + is-point-limit-function-Metric-Space X Y f x y → + is-classical-limit-map-Metric-Space X Y f x y + is-classical-limit-is-limit-map-Metric-Space H ε = + map-trunc-Prop (λ (μ , is-mod-μ) → (μ ε , is-mod-μ ε)) H +``` + +### Assuming countable choice, classical limits are constructive limits + +```agda +module _ + {l1 l2 l3 l4 : Level} + (acω : ACω) + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + (x : type-Metric-Space X) + (y : type-Metric-Space Y) + where + + abstract + is-limit-is-classical-limit-map-acω-Metric-Space : + is-classical-limit-map-Metric-Space X Y f x y → + is-point-limit-function-Metric-Space X Y f x y + is-limit-is-classical-limit-map-acω-Metric-Space H = + let + open + do-syntax-trunc-Prop + ( is-point-limit-prop-function-Metric-Space X Y f x y) + in do + μ ← + choice-countable-discrete-set-ACω + ( set-ℚ⁺) + ( is-countable-set-ℚ⁺) + ( has-decidable-equality-ℚ⁺) + ( acω) + ( λ ε → + Σ-Set + ( set-ℚ⁺) + ( λ δ → + set-Prop + ( Π-Prop + ( type-Metric-Space X) + ( λ x' → + neighborhood-prop-Metric-Space X δ x x' ⇒ + neighborhood-prop-Metric-Space Y ε y (f x'))))) + ( H) + intro-exists (pr1 ∘ μ) (pr2 ∘ μ) +``` + +## See also + +- [Constructive limits of functions in metric spaces](metric-spaces.limits-of-functions-metric-spaces.md) diff --git a/src/metric-spaces/classically-pointwise-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/classically-pointwise-continuous-functions-metric-spaces.lagda.md new file mode 100644 index 00000000000..28cf4e77faf --- /dev/null +++ b/src/metric-spaces/classically-pointwise-continuous-functions-metric-spaces.lagda.md @@ -0,0 +1,111 @@ +# Classically pointwise continuous functions in metric spaces + +```agda +module metric-spaces.classically-pointwise-continuous-functions-metric-spaces where +``` + +
Imports + +```agda +open import foundation.axiom-of-countable-choice +open import foundation.propositions +open import foundation.universe-levels + +open import metric-spaces.classical-limits-of-functions-metric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pointwise-continuous-functions-metric-spaces +``` + +
+ +## Idea + +A +{{#concept "classically pointwise continuous function" Disambiguation="between metric spaces" Agda=pointwise-continuous-map-Metric-Space}} +from a [metric space](metric-spaces.metric-spaces.md) `X` to a metric space `Y` +is a function `f : X → Y` such that for every `x : X`, the +[classical limit](metric-spaces.classical-limits-of-functions-metric-spaces.md) +of `f` as it approaches `x` is `f x`. + +## Definition + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + where + + is-classically-pointwise-continuous-prop-map-Metric-Space : + Prop (l1 ⊔ l2 ⊔ l4) + is-classically-pointwise-continuous-prop-map-Metric-Space = + Π-Prop + ( type-Metric-Space X) + ( λ x → is-classical-limit-prop-map-Metric-Space X Y f x (f x)) + + is-classically-pointwise-continuous-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) + is-classically-pointwise-continuous-map-Metric-Space = + type-Prop is-classically-pointwise-continuous-prop-map-Metric-Space +``` + +## Properties + +### Constructively pointwise continuous functions are classically pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : pointwise-continuous-map-Metric-Space X Y) + where + + abstract + is-classically-pointwise-continuous-pointwise-continuous-map-Metric-Space : + is-classically-pointwise-continuous-map-Metric-Space + ( X) + ( Y) + ( map-pointwise-continuous-map-Metric-Space X Y f) + is-classically-pointwise-continuous-pointwise-continuous-map-Metric-Space + x = + is-classical-limit-is-limit-map-Metric-Space + ( X) + ( Y) + ( map-pointwise-continuous-map-Metric-Space X Y f) + ( x) + ( map-pointwise-continuous-map-Metric-Space X Y f x) + ( is-pointwise-continuous-map-pointwise-continuous-map-Metric-Space + ( X) + ( Y) + ( f) + ( x)) +``` + +### Assuming countable choice, classically pointwise continuous functions are continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (acω : ACω) + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + where + + abstract + is-pointwise-continuous-is-classically-pointwise-continuous-map-acω-Metric-Space : + is-classically-pointwise-continuous-map-Metric-Space X Y f → + is-pointwise-continuous-map-Metric-Space X Y f + is-pointwise-continuous-is-classically-pointwise-continuous-map-acω-Metric-Space + H x = + is-limit-is-classical-limit-map-acω-Metric-Space + ( acω) + ( X) + ( Y) + ( f) + ( x) + ( f x) + ( H x) +``` diff --git a/src/metric-spaces/continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/continuity-of-functions-at-points-in-metric-spaces.lagda.md similarity index 78% rename from src/metric-spaces/continuous-functions-metric-spaces.lagda.md rename to src/metric-spaces/continuity-of-functions-at-points-in-metric-spaces.lagda.md index 36f6554f5fa..eadba773f73 100644 --- a/src/metric-spaces/continuous-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/continuity-of-functions-at-points-in-metric-spaces.lagda.md @@ -1,7 +1,7 @@ -# Continuous functions between metric spaces +# Continuity of functions at points in metric spaces ```agda -module metric-spaces.continuous-functions-metric-spaces where +module metric-spaces.continuity-of-functions-at-points-in-metric-spaces where ```
Imports @@ -68,21 +68,4 @@ module _ modulus-of-continuity-at-point-function-Metric-Space = type-subtype is-modulus-of-continuity-at-point-prop-function-Metric-Space - -module _ - {l1 l2 l3 l4 : Level} - (X : Metric-Space l1 l2) - (Y : Metric-Space l3 l4) - (f : type-function-Metric-Space X Y) - where - - is-pointwise-continuous-prop-function-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4) - is-pointwise-continuous-prop-function-Metric-Space = - Π-Prop - ( type-Metric-Space X) - ( is-continuous-at-point-prop-function-Metric-Space X Y f) - - is-pointwise-continuous-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) - is-pointwise-continuous-function-Metric-Space = - type-Prop is-pointwise-continuous-prop-function-Metric-Space ``` diff --git a/src/metric-spaces/dense-subsets-metric-spaces.lagda.md b/src/metric-spaces/dense-subsets-metric-spaces.lagda.md index 307f1829908..5b8be946001 100644 --- a/src/metric-spaces/dense-subsets-metric-spaces.lagda.md +++ b/src/metric-spaces/dense-subsets-metric-spaces.lagda.md @@ -20,6 +20,7 @@ open import foundation.universe-levels open import metric-spaces.closure-subsets-metric-spaces open import metric-spaces.metric-spaces +open import metric-spaces.pointwise-continuous-functions-metric-spaces open import metric-spaces.subspaces-metric-spaces ``` @@ -46,6 +47,24 @@ module _ is-dense-subset-Metric-Space : UU (l1 ⊔ l2 ⊔ l3) is-dense-subset-Metric-Space = type-Prop is-dense-prop-subset-Metric-Space + +dense-subset-Metric-Space : + {l1 l2 : Level} (l3 : Level) (X : Metric-Space l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l3) +dense-subset-Metric-Space l3 X = + type-subtype (is-dense-prop-subset-Metric-Space {l3 = l3} X) + +module _ + {l1 l2 l3 : Level} + (X : Metric-Space l1 l2) + (S : dense-subset-Metric-Space l3 X) + where + + subset-dense-subset-Metric-Space : subset-Metric-Space l3 X + subset-dense-subset-Metric-Space = pr1 S + + is-dense-subset-dense-subset-Metric-Space : + is-dense-subset-Metric-Space X subset-dense-subset-Metric-Space + is-dense-subset-dense-subset-Metric-Space = pr2 S ``` ## Properties diff --git a/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md b/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md index 5e49e6ee82f..3c8e5284629 100644 --- a/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md @@ -9,12 +9,8 @@ module metric-spaces.limits-of-functions-metric-spaces where ```agda open import elementary-number-theory.positive-rational-numbers -open import foundation.dependent-pair-types -open import foundation.existential-quantification open import foundation.inhabited-subtypes -open import foundation.propositional-truncations open import foundation.propositions -open import foundation.subtypes open import foundation.universe-levels open import metric-spaces.functions-metric-spaces @@ -71,3 +67,7 @@ module _ is-point-limit-function-Metric-Space = type-Prop is-point-limit-prop-function-Metric-Space ``` + +## See also + +- [Classical limits of functions in metric spaces](metric-spaces.classical-limits-of-functions-metric-spaces.md) diff --git a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md index 6da9948861f..023f6c84f5c 100644 --- a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md +++ b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md @@ -546,19 +546,19 @@ is-cauchy-approximation-rational-ℚ⁺ ε δ = ( rational-ℚ⁺ δ) ( rational-ℚ⁺ (ε +ℚ⁺ δ)) ( rational-ℚ⁺ ε +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))) - ( le-right-add-ℚ⁺ + ( le-left-add-ℚ⁺ ( ε) ( ε +ℚ⁺ δ)) - ( le-right-add-ℚ⁺ ε δ))) , + ( le-left-add-ℚ⁺ ε δ))) , ( leq-le-ℚ ( transitive-le-ℚ ( rational-ℚ⁺ ε) ( rational-ℚ⁺ (ε +ℚ⁺ δ)) ( rational-ℚ⁺ δ +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))) - ( le-right-add-ℚ⁺ + ( le-left-add-ℚ⁺ ( δ) ( ε +ℚ⁺ δ)) - ( le-left-add-ℚ⁺ ε δ))) + ( le-right-add-ℚ⁺ ε δ))) cauchy-approximation-rational-ℚ⁺ : cauchy-approximation-Metric-Space metric-space-ℚ @@ -582,7 +582,7 @@ is-zero-limit-rational-ℚ⁺ ε δ = ( inv-tr ( le-ℚ (rational-ℚ⁺ ε)) ( left-unit-law-add-ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))) - ( le-left-add-ℚ⁺ ε δ))) + ( le-right-add-ℚ⁺ ε δ))) convergent-rational-ℚ⁺ : convergent-cauchy-approximation-Metric-Space metric-space-ℚ diff --git a/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md index a505a4f9714..eb19b12fcf3 100644 --- a/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md @@ -22,7 +22,7 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cartesian-products-metric-spaces -open import metric-spaces.continuous-functions-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces open import metric-spaces.functions-metric-spaces open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-spaces diff --git a/src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md new file mode 100644 index 00000000000..54655cc0d92 --- /dev/null +++ b/src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md @@ -0,0 +1,367 @@ +# Pointwise continuous functions in metric spaces + +```agda +module metric-spaces.pointwise-continuous-functions-metric-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.minimum-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.cartesian-product-types +open import foundation.constant-maps +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-propositional-truncation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.cartesian-products-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.limits-of-functions-metric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.uniformly-continuous-functions-metric-spaces +``` + +
+ +## Idea + +A +{{#concept "pointwise continuous function" Disambiguation="between metric spaces" Agda=pointwise-continuous-map-Metric-Space}} +from a [metric space](metric-spaces.metric-spaces.md) `X` to a metric space `Y` +is a function `f : X → Y` which is +[continuous at every point](metric-spaces.continuity-of-functions-at-points-in-metric-spaces.md) +in `X`. + +## Definition + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + where + + is-pointwise-continuous-prop-map-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4) + is-pointwise-continuous-prop-map-Metric-Space = + Π-Prop + ( type-Metric-Space X) + ( is-continuous-at-point-prop-function-Metric-Space X Y f) + + is-pointwise-continuous-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) + is-pointwise-continuous-map-Metric-Space = + type-Prop is-pointwise-continuous-prop-map-Metric-Space + +pointwise-continuous-map-Metric-Space : + {l1 l2 l3 l4 : Level} → Metric-Space l1 l2 → Metric-Space l3 l4 → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +pointwise-continuous-map-Metric-Space X Y = + type-subtype (is-pointwise-continuous-prop-map-Metric-Space X Y) + +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : pointwise-continuous-map-Metric-Space X Y) + where + + map-pointwise-continuous-map-Metric-Space : + type-function-Metric-Space X Y + map-pointwise-continuous-map-Metric-Space = pr1 f + + is-pointwise-continuous-map-pointwise-continuous-map-Metric-Space : + is-pointwise-continuous-map-Metric-Space + ( X) + ( Y) + ( map-pointwise-continuous-map-Metric-Space) + is-pointwise-continuous-map-pointwise-continuous-map-Metric-Space = pr2 f +``` + +## Properties + +### The Cartesian product of pointwise continuous functions on metric spaces + +```agda +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l3 l4) + (C : Metric-Space l5 l6) (D : Metric-Space l7 l8) + (f : pointwise-continuous-map-Metric-Space A B) + (g : pointwise-continuous-map-Metric-Space C D) + where + + map-product-pointwise-continuous-map-Metric-Space : + type-Metric-Space A × type-Metric-Space C → + type-Metric-Space B × type-Metric-Space D + map-product-pointwise-continuous-map-Metric-Space = + map-product + ( map-pointwise-continuous-map-Metric-Space A B f) + ( map-pointwise-continuous-map-Metric-Space C D g) + + abstract + is-pointwise-continuous-map-product-pointwise-continuous-map-Metric-Space : + is-pointwise-continuous-map-Metric-Space + ( product-Metric-Space A C) + ( product-Metric-Space B D) + ( map-product-pointwise-continuous-map-Metric-Space) + is-pointwise-continuous-map-product-pointwise-continuous-map-Metric-Space + ( a , c) = + let + open + do-syntax-trunc-Prop + ( is-point-limit-prop-function-Metric-Space + ( product-Metric-Space A C) + ( product-Metric-Space B D) + ( map-product-pointwise-continuous-map-Metric-Space) + ( a , c) + ( map-product-pointwise-continuous-map-Metric-Space (a , c))) + in do + (μf , is-mod-μf) ← + is-pointwise-continuous-map-pointwise-continuous-map-Metric-Space + ( A) + ( B) + ( f) + ( a) + (μg , is-mod-μg) ← + is-pointwise-continuous-map-pointwise-continuous-map-Metric-Space + ( C) + ( D) + ( g) + ( c) + intro-exists + ( λ ε → min-ℚ⁺ (μf ε) (μg ε)) + ( λ ε (a' , c') (Naa' , Ncc') → + ( is-mod-μf + ( ε) + ( a') + ( weakly-monotonic-neighborhood-Metric-Space + ( A) + ( a) + ( a') + ( min-ℚ⁺ (μf ε) (μg ε)) + ( μf ε) + ( leq-left-min-ℚ⁺ (μf ε) (μg ε)) + ( Naa')) , + is-mod-μg + ( ε) + ( c') + ( weakly-monotonic-neighborhood-Metric-Space + ( C) + ( c) + ( c') + ( min-ℚ⁺ (μf ε) (μg ε)) + ( μg ε) + ( leq-right-min-ℚ⁺ (μf ε) (μg ε)) + ( Ncc')))) + + pointwise-continuous-map-product-Metric-Space : + pointwise-continuous-map-Metric-Space + ( product-Metric-Space A C) + ( product-Metric-Space B D) + pointwise-continuous-map-product-Metric-Space = + ( map-product-pointwise-continuous-map-Metric-Space , + is-pointwise-continuous-map-product-pointwise-continuous-map-Metric-Space) +``` + +### The composition of pointwise continuous functions + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (Z : Metric-Space l5 l6) + (f : pointwise-continuous-map-Metric-Space Y Z) + (g : pointwise-continuous-map-Metric-Space X Y) + where + + map-comp-pointwise-continuous-map-Metric-Space : + type-function-Metric-Space X Z + map-comp-pointwise-continuous-map-Metric-Space = + map-pointwise-continuous-map-Metric-Space Y Z f ∘ + map-pointwise-continuous-map-Metric-Space X Y g + + abstract + is-pointwise-continuous-map-comp-pointwise-continuous-map-Metric-Space : + is-pointwise-continuous-map-Metric-Space X Z + ( map-comp-pointwise-continuous-map-Metric-Space) + is-pointwise-continuous-map-comp-pointwise-continuous-map-Metric-Space + x = + let + open + do-syntax-trunc-Prop + ( is-point-limit-prop-function-Metric-Space X Z + ( map-comp-pointwise-continuous-map-Metric-Space) + ( x) + ( map-comp-pointwise-continuous-map-Metric-Space x)) + in do + (μg , is-mod-μg) ← + is-pointwise-continuous-map-pointwise-continuous-map-Metric-Space + ( X) + ( Y) + ( g) + ( x) + (μf , is-mod-μf) ← + is-pointwise-continuous-map-pointwise-continuous-map-Metric-Space + ( Y) + ( Z) + ( f) + ( map-pointwise-continuous-map-Metric-Space X Y g x) + intro-exists + ( μg ∘ μf) + ( λ ε x' Nxx' → + is-mod-μf + ( ε) + ( map-pointwise-continuous-map-Metric-Space X Y g x') + ( is-mod-μg (μf ε) x' Nxx')) + + comp-pointwise-continuous-map-Metric-Space : + pointwise-continuous-map-Metric-Space X Z + comp-pointwise-continuous-map-Metric-Space = + ( map-comp-pointwise-continuous-map-Metric-Space , + is-pointwise-continuous-map-comp-pointwise-continuous-map-Metric-Space) +``` + +### Uniformly continuous functions are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + where + + abstract + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space : + (f : type-function-Metric-Space X Y) → + is-uniformly-continuous-function-Metric-Space X Y f → + is-pointwise-continuous-map-Metric-Space X Y f + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space + f H x = map-trunc-Prop (λ (μ , is-mod-μ) → (μ , is-mod-μ x)) H + + pointwise-continuous-uniformly-continuous-function-Metric-Space : + uniformly-continuous-function-Metric-Space X Y → + pointwise-continuous-map-Metric-Space X Y + pointwise-continuous-uniformly-continuous-function-Metric-Space (f , H) = + ( f , + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space f H) +``` + +### Short functions are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + where + + abstract + is-pointwise-continuous-is-short-function-Metric-Space : + (f : type-function-Metric-Space X Y) → + is-short-function-Metric-Space X Y f → + is-pointwise-continuous-map-Metric-Space X Y f + is-pointwise-continuous-is-short-function-Metric-Space + f H = + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space + ( X) + ( Y) + ( f) + ( is-uniformly-continuous-is-short-function-Metric-Space X Y f H) + + pointwise-continuous-short-function-Metric-Space : + short-function-Metric-Space X Y → + pointwise-continuous-map-Metric-Space X Y + pointwise-continuous-short-function-Metric-Space (f , H) = + ( f , + is-pointwise-continuous-is-short-function-Metric-Space f H) +``` + +### Isometries are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + where + + abstract + is-pointwise-continuous-is-isometry-Metric-Space : + (f : type-function-Metric-Space X Y) → + is-isometry-Metric-Space X Y f → + is-pointwise-continuous-map-Metric-Space X Y f + is-pointwise-continuous-is-isometry-Metric-Space + f H = + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space + ( X) + ( Y) + ( f) + ( is-uniformly-continuous-is-isometry-Metric-Space X Y f H) + + pointwise-continuous-isometry-Metric-Space : + isometry-Metric-Space X Y → + pointwise-continuous-map-Metric-Space X Y + pointwise-continuous-isometry-Metric-Space (f , H) = + ( f , + is-pointwise-continuous-is-isometry-Metric-Space f H) +``` + +### Constant functions between metric spaces are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (y : type-Metric-Space Y) + where + + abstract + is-pointwise-continuous-const-Metric-Space : + is-pointwise-continuous-map-Metric-Space + ( X) + ( Y) + ( const (type-Metric-Space X) y) + is-pointwise-continuous-const-Metric-Space = + is-pointwise-continuous-is-short-function-Metric-Space X Y _ + ( is-short-constant-function-Metric-Space X Y y) + + const-pointwise-continuous-map-Metric-Space : + pointwise-continuous-map-Metric-Space X Y + const-pointwise-continuous-map-Metric-Space = + pointwise-continuous-short-function-Metric-Space X Y + ( short-constant-function-Metric-Space X Y y) +``` + +### The identity function is a pointwise continuous function on any metric space + +```agda +module _ + {l1 l2 : Level} + (X : Metric-Space l1 l2) + where + + abstract + is-pointwise-continuous-map-id-Metric-Space : + is-pointwise-continuous-map-Metric-Space X X id + is-pointwise-continuous-map-id-Metric-Space = + is-pointwise-continuous-is-isometry-Metric-Space X X id + ( is-isometry-id-Metric-Space X) + + id-pointwise-continuous-map-Metric-Space : + pointwise-continuous-map-Metric-Space X X + id-pointwise-continuous-map-Metric-Space = + ( id , is-pointwise-continuous-map-id-Metric-Space) +``` diff --git a/src/metric-spaces/rational-approximations-of-zero.lagda.md b/src/metric-spaces/rational-approximations-of-zero.lagda.md index 1af8b5b5d2a..c6ee20358a5 100644 --- a/src/metric-spaces/rational-approximations-of-zero.lagda.md +++ b/src/metric-spaces/rational-approximations-of-zero.lagda.md @@ -182,7 +182,7 @@ module _ ( f ε -ℚ zero-ℚ)) ( rational-ℚ⁺ ε) ( rational-ℚ⁺ (ε +ℚ⁺ δ)) - ( leq-le-ℚ⁺ {ε} {ε +ℚ⁺ δ} (le-left-add-ℚ⁺ ε δ)) + ( leq-le-ℚ⁺ {ε} {ε +ℚ⁺ δ} (le-right-add-ℚ⁺ ε δ)) ( inv-tr ( λ y → leq-ℚ (rational-ℚ⁰⁺ y) (rational-ℚ⁺ ε)) ( right-zero-law-dist-ℚ diff --git a/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md b/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md index 15a417ce7d2..3470843988f 100644 --- a/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md +++ b/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md @@ -209,5 +209,5 @@ module _ neighborhood-Rational-Neighborhood-Relation N δ x y) iff-le-neighborhood-saturated-monotonic-Rational-Neighborhood-Relation ε x y = ( λ Nxy δ ε<δ → monotonic-N x y ε δ ε<δ Nxy) , - ( λ H → saturated-N ε x y λ δ → H (ε +ℚ⁺ δ) (le-left-add-ℚ⁺ ε δ)) + ( λ H → saturated-N ε x y λ δ → H (ε +ℚ⁺ δ) (le-right-add-ℚ⁺ ε δ)) ``` diff --git a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md index edbb096acc9..efdb75cd298 100644 --- a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md @@ -23,7 +23,7 @@ open import foundation.universe-levels open import logic.functoriality-existential-quantification -open import metric-spaces.continuous-functions-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces open import metric-spaces.functions-metric-spaces open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-spaces diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index 538d9ef2590..08f6ce1936e 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -154,6 +154,7 @@ open import order-theory.strictly-inflationary-maps-strict-preorders public open import order-theory.strictly-preordered-sets public open import order-theory.subposets public open import order-theory.subpreorders public +open import order-theory.subtypes-strict-preorders public open import order-theory.suplattices public open import order-theory.supremum-preserving-maps-posets public open import order-theory.top-elements-large-posets public diff --git a/src/order-theory/subtypes-strict-preorders.lagda.md b/src/order-theory/subtypes-strict-preorders.lagda.md new file mode 100644 index 00000000000..c4149bbf042 --- /dev/null +++ b/src/order-theory/subtypes-strict-preorders.lagda.md @@ -0,0 +1,67 @@ +# Subtypes of strict preorders + +```agda +module order-theory.subtypes-strict-preorders where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.strict-preorders +``` + +
+ +## Idea + +Any [subtype](foundation.subtypes.md) of the underlying type of a +[strict preorder](order-theory.strict-preorders.md) inherits the structure of a +strict preorder. + +## Definition + +```agda +subtype-Strict-Preorder : + {l1 l2 : Level} (l : Level) → Strict-Preorder l1 l2 → UU (l1 ⊔ lsuc l) +subtype-Strict-Preorder l P = subtype l (type-Strict-Preorder P) + +module _ + {l1 l2 l3 : Level} + (P : Strict-Preorder l1 l2) + (S : subtype-Strict-Preorder l3 P) + where + + type-subtype-Strict-Preorder : UU (l1 ⊔ l3) + type-subtype-Strict-Preorder = type-subtype S + + le-prop-subtype-Strict-Preorder : + Relation-Prop l2 type-subtype-Strict-Preorder + le-prop-subtype-Strict-Preorder (x , x∈S) (y , y∈S) = + le-prop-Strict-Preorder P x y + + le-subtype-Strict-Preorder : Relation l2 type-subtype-Strict-Preorder + le-subtype-Strict-Preorder = + type-Relation-Prop le-prop-subtype-Strict-Preorder + + is-irreflexive-le-subtype-Strict-Preorder : + is-irreflexive le-subtype-Strict-Preorder + is-irreflexive-le-subtype-Strict-Preorder (x , x∈S) = + is-irreflexive-le-Strict-Preorder P x + + is-transitive-le-subtype-Strict-Preorder : + is-transitive le-subtype-Strict-Preorder + is-transitive-le-subtype-Strict-Preorder (x , x∈S) (y , y∈S) (z , z∈S) = + is-transitive-le-Strict-Preorder P x y z + + strict-preorder-subtype-Strict-Preorder : Strict-Preorder (l1 ⊔ l3) l2 + strict-preorder-subtype-Strict-Preorder = + ( type-subtype-Strict-Preorder , + le-prop-subtype-Strict-Preorder , + is-irreflexive-le-subtype-Strict-Preorder , + is-transitive-le-subtype-Strict-Preorder) +``` diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 8210a60b2e8..cb169f8041f 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -22,8 +22,11 @@ open import real-numbers.binary-maximum-real-numbers public open import real-numbers.binary-minimum-real-numbers public open import real-numbers.cauchy-completeness-dedekind-real-numbers public open import real-numbers.cauchy-sequences-real-numbers public +open import real-numbers.classical-limits-of-functions-real-numbers public +open import real-numbers.classically-pointwise-continuous-functions-real-numbers public open import real-numbers.closed-intervals-real-numbers public open import real-numbers.dedekind-real-numbers public +open import real-numbers.dense-subsets-real-numbers public open import real-numbers.difference-real-numbers public open import real-numbers.distance-real-numbers public open import real-numbers.enclosing-closed-rational-intervals-real-numbers public @@ -32,6 +35,7 @@ open import real-numbers.extensionality-multiplication-bilinear-form-real-number open import real-numbers.field-of-real-numbers public open import real-numbers.finitely-enumerable-subsets-real-numbers public open import real-numbers.geometric-sequences-real-numbers public +open import real-numbers.increasing-functions-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 @@ -52,6 +56,7 @@ open import real-numbers.large-additive-group-of-real-numbers public open import real-numbers.large-multiplicative-group-of-positive-real-numbers public open import real-numbers.large-multiplicative-monoid-of-real-numbers public open import real-numbers.large-ring-of-real-numbers public +open import real-numbers.limits-of-functions-real-numbers public open import real-numbers.limits-sequences-real-numbers public open import real-numbers.lipschitz-continuity-multiplication-real-numbers public open import real-numbers.local-ring-of-real-numbers public @@ -82,11 +87,13 @@ open import real-numbers.negation-real-numbers public open import real-numbers.negative-real-numbers public open import real-numbers.nonnegative-real-numbers public open import real-numbers.nonzero-real-numbers public +open import real-numbers.pointwise-continuous-functions-real-numbers public open import real-numbers.positive-and-negative-real-numbers public open import real-numbers.positive-real-numbers public open import real-numbers.powers-real-numbers public open import real-numbers.proper-closed-intervals-real-numbers public open import real-numbers.raising-universe-levels-real-numbers public +open import real-numbers.rational-approximates-of-real-numbers public open import real-numbers.rational-lower-dedekind-real-numbers public open import real-numbers.rational-real-numbers public open import real-numbers.rational-upper-dedekind-real-numbers public @@ -106,6 +113,7 @@ open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbe 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 +open import real-numbers.strictly-increasing-functions-real-numbers public open import real-numbers.subsets-real-numbers public open import real-numbers.suprema-families-real-numbers public open import real-numbers.totally-bounded-subsets-real-numbers public diff --git a/src/real-numbers/addition-positive-real-numbers.lagda.md b/src/real-numbers/addition-positive-real-numbers.lagda.md index b56c02b5cb8..b24d21f5183 100644 --- a/src/real-numbers/addition-positive-real-numbers.lagda.md +++ b/src/real-numbers/addition-positive-real-numbers.lagda.md @@ -84,15 +84,19 @@ abstract opaque ( right-unit-law-add-ℝ x) ( preserves-le-left-add-ℝ x zero-ℝ d pos-d) -le-right-add-real-ℝ⁺ : - {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → le-ℝ x (real-ℝ⁺ d +ℝ x) -le-right-add-real-ℝ⁺ x d = - tr (le-ℝ x) (commutative-add-ℝ x (real-ℝ⁺ d)) (le-left-add-real-ℝ⁺ x d) - abstract + le-right-add-real-ℝ⁺ : + {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → le-ℝ x (real-ℝ⁺ d +ℝ x) + le-right-add-real-ℝ⁺ x d = + tr (le-ℝ x) (commutative-add-ℝ x (real-ℝ⁺ d)) (le-left-add-real-ℝ⁺ x d) + leq-left-add-real-ℝ⁺ : {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → leq-ℝ x (x +ℝ real-ℝ⁺ d) leq-left-add-real-ℝ⁺ x d = leq-le-ℝ (le-left-add-real-ℝ⁺ x d) + + leq-right-add-real-ℝ⁺ : + {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → leq-ℝ x (real-ℝ⁺ d +ℝ x) + leq-right-add-real-ℝ⁺ x d = leq-le-ℝ (le-right-add-real-ℝ⁺ x d) ``` ### Subtraction by a positive real number is a strictly deflationary map diff --git a/src/real-numbers/classical-limits-of-functions-real-numbers.lagda.md b/src/real-numbers/classical-limits-of-functions-real-numbers.lagda.md new file mode 100644 index 00000000000..afae4c7216d --- /dev/null +++ b/src/real-numbers/classical-limits-of-functions-real-numbers.lagda.md @@ -0,0 +1,98 @@ +# Classical limits of functions on the real numbers + +```agda +module real-numbers.classical-limits-of-functions-real-numbers where +``` + +
Imports + +```agda +open import foundation.axiom-of-countable-choice +open import foundation.propositions +open import foundation.universe-levels + +open import metric-spaces.classical-limits-of-functions-metric-spaces + +open import real-numbers.dedekind-real-numbers +open import real-numbers.limits-of-functions-real-numbers +open import real-numbers.metric-space-of-real-numbers +``` + +
+ +## Idea + +The +{{#concept "classical definition of a limit" Disambiguation="in ℝ" Agda=is-classical-limit-function-ℝ}} +states that the limit of `f x` as `x` approaches `x₀` is a `y` such that for any +`ε : ℚ⁺`, there [exists](foundation.existential-quantification.md) a `δ : ℚ⁺` +such that if `x` and `x₀` are in a `δ`-neighborhood of each other, `f x` and `y` +are in a `ε`-neighborhood of each other. + +## Definition + +```agda +is-classical-limit-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → Prop (lsuc l1 ⊔ l2) +is-classical-limit-prop-function-ℝ {l1} {l2} = + is-classical-limit-prop-map-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + +is-classical-limit-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → UU (lsuc l1 ⊔ l2) +is-classical-limit-function-ℝ f x y = + type-Prop (is-classical-limit-prop-function-ℝ f x y) +``` + +## Properties + +### Constructive limits are classical limits + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + (x : ℝ l1) + (y : ℝ l2) + where + + abstract + is-classical-limit-is-limit-function-ℝ : + is-limit-function-ℝ f x y → is-classical-limit-function-ℝ f x y + is-classical-limit-is-limit-function-ℝ = + is-classical-limit-is-limit-map-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) + ( x) + ( y) +``` + +### Assuming countable choice, classical limits are constructive limits + +```agda +module _ + {l1 l2 : Level} + (acω : ACω) + (f : ℝ l1 → ℝ l2) + (x : ℝ l1) + (y : ℝ l2) + where + + abstract + is-limit-is-classical-limit-ACω-function-ℝ : + is-classical-limit-function-ℝ f x y → is-limit-function-ℝ f x y + is-limit-is-classical-limit-ACω-function-ℝ = + is-limit-is-classical-limit-map-acω-Metric-Space + ( acω) + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) + ( x) + ( y) +``` + +## See also + +- [Constructive limits of functions on the real numbers](real-numbers.limits-of-functions-real-numbers.md) diff --git a/src/real-numbers/classically-pointwise-continuous-functions-real-numbers.lagda.md b/src/real-numbers/classically-pointwise-continuous-functions-real-numbers.lagda.md new file mode 100644 index 00000000000..d050687e084 --- /dev/null +++ b/src/real-numbers/classically-pointwise-continuous-functions-real-numbers.lagda.md @@ -0,0 +1,98 @@ +# Classically pointwise continuous functions on the real numbers + +```agda +module real-numbers.classically-pointwise-continuous-functions-real-numbers where +``` + +
Imports + +```agda +open import foundation.axiom-of-countable-choice +open import foundation.propositions +open import foundation.universe-levels + +open import metric-spaces.classically-pointwise-continuous-functions-metric-spaces + +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.pointwise-continuous-functions-real-numbers +``` + +
+ +## Idea + +A +{{#concept "classically pointwise continuous function" Disambiguation="from ℝ to ℝ" Agda=is-classically-pointwise-continuous-map-ℝ}} +from the [real numbers](real-numbers.dedekind-real-numbers.md) to themselves is +a +[classically pointwise continuous function](metric-spaces.classically-pointwise-continuous-functions-metric-spaces.md) +from the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md) to +itself. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + is-classically-pointwise-continuous-prop-function-ℝ : Prop (lsuc l1 ⊔ l2) + is-classically-pointwise-continuous-prop-function-ℝ = + is-classically-pointwise-continuous-prop-map-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) + + is-classically-pointwise-continuous-map-ℝ : UU (lsuc l1 ⊔ l2) + is-classically-pointwise-continuous-map-ℝ = + type-Prop is-classically-pointwise-continuous-prop-function-ℝ +``` + +## Properties + +### Constructively pointwise continuous functions are classically pointwise continuous + +```agda +module _ + {l1 l2 : Level} + (f : pointwise-continuous-map-ℝ l1 l2) + where + + abstract + is-classically-pointwise-continuous-pointwise-continuous-map-ℝ : + is-classically-pointwise-continuous-map-ℝ + ( map-pointwise-continuous-map-ℝ f) + is-classically-pointwise-continuous-pointwise-continuous-map-ℝ = + is-classically-pointwise-continuous-pointwise-continuous-map-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) +``` + +### Assuming countable choice, the classical definition of continuity implies the constructive definition + +```agda +module _ + {l1 l2 : Level} + (acω : ACω) + (f : ℝ l1 → ℝ l2) + where + + abstract + is-pointwise-continuous-is-classically-pointwise-continuous-ACω-function-ℝ : + is-classically-pointwise-continuous-map-ℝ f → + is-pointwise-continuous-map-ℝ f + is-pointwise-continuous-is-classically-pointwise-continuous-ACω-function-ℝ = + is-pointwise-continuous-is-classically-pointwise-continuous-map-acω-Metric-Space + ( acω) + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) +``` + +## See also + +- [Constructively pointwise continuous functions on the real numbers](real-numbers.pointwise-continuous-functions-real-numbers.md) diff --git a/src/real-numbers/dense-subsets-real-numbers.lagda.md b/src/real-numbers/dense-subsets-real-numbers.lagda.md new file mode 100644 index 00000000000..e79e7552ca6 --- /dev/null +++ b/src/real-numbers/dense-subsets-real-numbers.lagda.md @@ -0,0 +1,416 @@ +# Dense subsets of the real numbers + +```agda +module real-numbers.dense-subsets-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.minimum-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.intersections-subtypes +open import foundation.propositional-truncations +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +open import metric-spaces.dense-subsets-metric-spaces + +open import order-theory.large-posets + +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-approximates-of-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.subsets-real-numbers +``` + +
+ +## Idea + +A {{#concept "dense subset" Disambiguation="of ℝ" Agda=dense-subset-ℝ}} of the +[real numbers](real-numbers.dedekind-real-numbers.md) `ℝ` is a +[dense subset](metric-spaces.dense-subsets-metric-spaces.md) of the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md), +which means that it is a [subset](real-numbers.subsets-real-numbers.md) `S ⊆ ℝ` +such that for any `x : ℝ` and any +[positive rational](elementary-number-theory.positive-rational-numbers.md) `ε`, +there is a `y` in an `ε`-neighborhood of `X` that is also in `S`. + +## Definition + +```agda +is-dense-subset-ℝ : {l1 l2 : Level} → subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2) +is-dense-subset-ℝ = is-dense-subset-Metric-Space (metric-space-ℝ _) + +dense-subset-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +dense-subset-ℝ l1 l2 = dense-subset-Metric-Space l1 (metric-space-ℝ l2) + +subset-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → subset-ℝ l1 l2 +subset-dense-subset-ℝ = pr1 + +is-dense-subset-dense-subset-ℝ : + {l1 l2 : Level} (S : dense-subset-ℝ l1 l2) (x : ℝ l2) (ε : ℚ⁺) → + intersect-subtype (neighborhood-prop-ℝ l2 ε x) (subset-dense-subset-ℝ S) +is-dense-subset-dense-subset-ℝ = pr2 + +type-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2) +type-dense-subset-ℝ S = type-subtype (subset-dense-subset-ℝ S) + +inclusion-dense-subset-ℝ : + {l1 l2 : Level} (S : dense-subset-ℝ l1 l2) → + type-dense-subset-ℝ S → ℝ l2 +inclusion-dense-subset-ℝ S = inclusion-subtype (subset-dense-subset-ℝ S) + +is-in-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → ℝ l2 → UU l1 +is-in-dense-subset-ℝ S = + is-in-subtype (subset-dense-subset-ℝ S) +``` + +## Properties + +### The rational reals are dense in `ℝ` + +```agda +abstract + is-dense-rational-real-ℝ : + (l : Level) → is-dense-subset-ℝ (subtype-rational-real {l}) + is-dense-rational-real-ℝ l x ε = + map-exists + ( _) + ( raise-real-ℚ l) + ( λ q Nεxq → ( Nεxq , q , is-rational-raise-real-ℚ l q)) + ( exists-rational-approximate-ℝ x ε) + +dense-subset-rational-real-ℝ : + (l : Level) → dense-subset-ℝ l l +dense-subset-rational-real-ℝ l = + ( subtype-rational-real , is-dense-rational-real-ℝ l) +``` + +### Given a dense subset `S ⊆ R`, two reals `x < y`, and positive rationals `δx`, `δy`, there are `x' < y'` with `x' ∈ S`, `y' ∈ S`, `x'` in a `δx`-neighborhood of `x` and correspondingly for `y` + +```agda +module _ + {l1 l2 : Level} + (S : dense-subset-ℝ l1 l2) + where + + abstract + exist-close-le-elements-dense-subset-ℝ : + {x y : ℝ l2} (δx δy : ℚ⁺) → le-ℝ x y → + exists + ( type-dense-subset-ℝ S × type-dense-subset-ℝ S) + ( λ ((x' , x'∈S) , (y' , y'∈S)) → + ( le-prop-ℝ x' y') ∧ + ( neighborhood-prop-ℝ l2 δx x x') ∧ + ( neighborhood-prop-ℝ l2 δy y y')) + exist-close-le-elements-dense-subset-ℝ {x} {y} δx δy xImports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.minimum-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.coproduct-types +open import foundation.dependent-pair-types +open import foundation.double-negation +open import foundation.empty-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.universe-levels + +open import order-theory.large-posets +open import order-theory.order-preserving-maps-posets +open import order-theory.posets +open import order-theory.subposets + +open import real-numbers.addition-real-numbers +open import real-numbers.classically-pointwise-continuous-functions-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.dense-subsets-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.pointwise-continuous-functions-real-numbers +open import real-numbers.rational-approximates-of-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.subsets-real-numbers +``` + +
+ +## Idea + +A function `f` from the [real numbers](real-numbers.dedekind-real-numbers.md) to +themselves is +{{#concept "increasing" Disambiguation="function from ℝ to ℝ" Agda=is-increasing-function-ℝ}} +if for all `x ≤ y`, `f x ≤ f y`; in other words, it is an +[order-preserving map](order-theory.order-preserving-maps-posets.md) on the +[poset of real numbers](real-numbers.inequality-real-numbers.md). + +Several arguments on this page are due to +[Mark Saving](https://math.stackexchange.com/users/798694/mark-saving) in this +Mathematics Stack Exchange answer: . + +## Definition + +```agda +is-increasing-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → Prop (lsuc l1 ⊔ l2) +is-increasing-prop-function-ℝ {l1} {l2} = + preserves-order-prop-Poset (ℝ-Poset l1) (ℝ-Poset l2) + +is-increasing-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → UU (lsuc l1 ⊔ l2) +is-increasing-function-ℝ f = type-Prop (is-increasing-prop-function-ℝ f) + +is-increasing-on-subset-function-ℝ : + {l1 l2 l3 : Level} (f : ℝ l1 → ℝ l2) (S : subset-ℝ l3 l1) → + UU (lsuc l1 ⊔ l2 ⊔ l3) +is-increasing-on-subset-function-ℝ f S = + preserves-order-Poset + ( poset-Subposet (ℝ-Poset _) S) + ( ℝ-Poset _) + ( f ∘ inclusion-subset-ℝ S) +``` + +## Properties + +### If `x < y` implies `f x ≤ f y`, then `f` is increasing + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + abstract + is-increasing-is-increasing-on-strict-inequalities-ℝ : + ((x y : ℝ l1) → le-ℝ x y → leq-ℝ (f x) (f y)) → + is-increasing-function-ℝ f + is-increasing-is-increasing-on-strict-inequalities-ℝ H x y x≤y = + double-negation-elim-leq-ℝ + ( f x) + ( f y) + ( map-double-negation + ( rec-coproduct + ( λ x~y → leq-eq-ℝ (ap f (eq-sim-ℝ x~y))) + ( H x y)) + ( irrefutable-sim-or-le-leq-ℝ x y x≤y)) + +module _ + {l1 l2 l3 : Level} + (f : ℝ l1 → ℝ l2) + (S : subset-ℝ l3 l1) + where + + abstract + is-increasing-is-increasing-on-strict-inequalities-on-subset-function-ℝ : + ( ((x y : type-subset-ℝ S) → + le-ℝ (pr1 x) (pr1 y) → leq-ℝ (f (pr1 x)) (f (pr1 y)))) → + is-increasing-on-subset-function-ℝ f S + is-increasing-is-increasing-on-strict-inequalities-on-subset-function-ℝ + H (x , x∈S) (y , y∈S) x≤y = + double-negation-elim-leq-ℝ + ( f x) + ( f y) + ( map-double-negation + ( rec-coproduct + ( λ x~y → leq-eq-ℝ (ap f (eq-sim-ℝ x~y))) + ( H (x , x∈S) (y , y∈S))) + ( irrefutable-sim-or-le-leq-ℝ x y x≤y)) +``` + +### If a pointwise continuous function `f` is increasing on a dense subset of `ℝ`, then it is increasing on `ℝ` + +```agda +module _ + {l1 l2 l3 : Level} + (f : pointwise-continuous-map-ℝ l1 l2) + (S : dense-subset-ℝ l3 l1) + where + + abstract + is-increasing-is-increasing-dense-subset-pointwise-continuous-map-ℝ : + is-increasing-on-subset-function-ℝ + ( map-pointwise-continuous-map-ℝ f) + ( subset-dense-subset-ℝ S) → + is-increasing-function-ℝ (map-pointwise-continuous-map-ℝ f) + is-increasing-is-increasing-dense-subset-pointwise-continuous-map-ℝ H = + let + f' = map-pointwise-continuous-map-ℝ f + open do-syntax-trunc-Prop empty-Prop + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + is-increasing-is-increasing-on-strict-inequalities-ℝ + ( map-pointwise-continuous-map-ℝ f) + ( λ x y xImports + +```agda +open import foundation.propositions +open import foundation.universe-levels + +open import metric-spaces.limits-of-functions-metric-spaces + +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-space-of-real-numbers +``` + + + +## Idea + +A +{{#concept "limit" Disambiguation="of a function from ℝ to ℝ" Agda=is-limit-function-ℝ}} +of a function `f` from the [real numbers](real-numbers.dedekind-real-numbers.md) +to themselves at `x : ℝ` is the +[limit](metric-spaces.limits-of-functions-metric-spaces.md) of `f` at `x` in the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). + +## Definition + +```agda +is-limit-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → Prop (lsuc l1 ⊔ l2) +is-limit-prop-function-ℝ {l1} {l2} = + is-point-limit-prop-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + +is-limit-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → UU (lsuc l1 ⊔ l2) +is-limit-function-ℝ f x y = type-Prop (is-limit-prop-function-ℝ f x y) +``` + +## See also + +- [Classical limits of functions on the real numbers](real-numbers.classical-limits-of-functions-real-numbers.md) 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 f33d4630f16..bb2edfbe6c2 100644 --- a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md +++ b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md @@ -29,8 +29,9 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cartesian-products-metric-spaces -open import metric-spaces.continuous-functions-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces open import metric-spaces.lipschitz-functions-metric-spaces +open import metric-spaces.pointwise-continuous-functions-metric-spaces open import metric-spaces.uniformly-continuous-functions-metric-spaces open import order-theory.large-posets @@ -323,7 +324,7 @@ This remains to be shown. abstract is-pointwise-continuous-mul-ℝ : (l1 l2 : Level) → - is-pointwise-continuous-function-Metric-Space + is-pointwise-continuous-map-Metric-Space ( product-Metric-Space (metric-space-ℝ l1) (metric-space-ℝ l2)) ( metric-space-ℝ (l1 ⊔ l2)) ( ind-Σ mul-ℝ) diff --git a/src/real-numbers/metric-space-of-real-numbers.lagda.md b/src/real-numbers/metric-space-of-real-numbers.lagda.md index a5f9e1bc435..21e16b10ec5 100644 --- a/src/real-numbers/metric-space-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-space-of-real-numbers.lagda.md @@ -12,6 +12,7 @@ module real-numbers.metric-space-of-real-numbers where open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.inequality-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers @@ -386,6 +387,17 @@ module _ ( right-leq-real-bound-neighborhood-ℝ d x y H)) ``` +### The neighborhood relation on the real numbers is weakly monotonic + +```agda +abstract + weakly-monotonic-neighborhood-ℝ : + {l : Level} (x y : ℝ l) (d₁ d₂ : ℚ⁺) → leq-ℚ⁺ d₁ d₂ → + neighborhood-ℝ l d₁ x y → neighborhood-ℝ l d₂ x y + weakly-monotonic-neighborhood-ℝ {l} = + weakly-monotonic-neighborhood-Metric-Space (metric-space-ℝ l) +``` + ### The canonical embedding from rational to real numbers is an isometry between metric spaces ```agda diff --git a/src/real-numbers/pointwise-continuous-functions-real-numbers.lagda.md b/src/real-numbers/pointwise-continuous-functions-real-numbers.lagda.md new file mode 100644 index 00000000000..6cefb4b1a18 --- /dev/null +++ b/src/real-numbers/pointwise-continuous-functions-real-numbers.lagda.md @@ -0,0 +1,72 @@ +# Pointwise continuous functions on the real numbers + +```agda +module real-numbers.pointwise-continuous-functions-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.axiom-of-countable-choice +open import foundation.dependent-pair-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.pointwise-continuous-functions-metric-spaces + +open import real-numbers.dedekind-real-numbers +open import real-numbers.limits-of-functions-real-numbers +open import real-numbers.metric-space-of-real-numbers +``` + +
+ +## Idea + +A +{{#concept "pointwise continuous function" Disambiguation="from ℝ to ℝ" Agda=pointwise-continuous-map-ℝ}} +from the [real numbers](real-numbers.dedekind-real-numbers.md) to the real +numbers is a +[pointwise continuous function](metric-spaces.pointwise-continuous-functions-metric-spaces.md) +from the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md) to +itself. + +## Definition + +```agda +is-pointwise-continuous-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → Prop (lsuc l1 ⊔ l2) +is-pointwise-continuous-prop-function-ℝ {l1} {l2} = + is-pointwise-continuous-prop-map-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + +is-pointwise-continuous-map-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → UU (lsuc l1 ⊔ l2) +is-pointwise-continuous-map-ℝ f = + type-Prop (is-pointwise-continuous-prop-function-ℝ f) + +pointwise-continuous-map-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +pointwise-continuous-map-ℝ l1 l2 = + type-subtype (is-pointwise-continuous-prop-function-ℝ {l1} {l2}) + +module _ + {l1 l2 : Level} + (f : pointwise-continuous-map-ℝ l1 l2) + where + + map-pointwise-continuous-map-ℝ : ℝ l1 → ℝ l2 + map-pointwise-continuous-map-ℝ = pr1 f + + is-pointwise-continuous-map-pointwise-continuous-map-ℝ : + is-pointwise-continuous-map-ℝ map-pointwise-continuous-map-ℝ + is-pointwise-continuous-map-pointwise-continuous-map-ℝ = pr2 f +``` + +## See also + +- [Classically pointwise continuous functions on the real numbers](real-numbers.classically-pointwise-continuous-functions-real-numbers.md) diff --git a/src/real-numbers/powers-real-numbers.lagda.md b/src/real-numbers/powers-real-numbers.lagda.md index a058eff222a..ac742c7c2bf 100644 --- a/src/real-numbers/powers-real-numbers.lagda.md +++ b/src/real-numbers/powers-real-numbers.lagda.md @@ -23,19 +23,26 @@ open import elementary-number-theory.rational-numbers open import elementary-number-theory.ring-of-rational-numbers open import foundation.action-on-identifications-functions +open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositional-truncations open import foundation.transport-along-identifications open import foundation.universe-levels +open import metric-spaces.cartesian-products-metric-spaces +open import metric-spaces.pointwise-continuous-functions-metric-spaces + open import order-theory.large-posets open import real-numbers.absolute-value-real-numbers open import real-numbers.dedekind-real-numbers +open import real-numbers.increasing-functions-real-numbers open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.large-ring-of-real-numbers +open import real-numbers.lipschitz-continuity-multiplication-real-numbers +open import real-numbers.metric-space-of-real-numbers open import real-numbers.multiplication-nonnegative-real-numbers open import real-numbers.multiplication-positive-and-negative-real-numbers open import real-numbers.multiplication-positive-real-numbers @@ -43,6 +50,7 @@ open import real-numbers.multiplication-real-numbers open import real-numbers.negation-real-numbers open import real-numbers.negative-real-numbers open import real-numbers.nonnegative-real-numbers +open import real-numbers.pointwise-continuous-functions-real-numbers open import real-numbers.positive-and-negative-real-numbers open import real-numbers.positive-real-numbers open import real-numbers.raising-universe-levels-real-numbers @@ -51,6 +59,7 @@ open import real-numbers.real-sequences-approximating-zero open import real-numbers.similarity-real-numbers open import real-numbers.squares-real-numbers open import real-numbers.strict-inequality-real-numbers +open import real-numbers.strictly-increasing-functions-real-numbers ``` @@ -75,6 +84,34 @@ power-ℝ = power-Large-Commutative-Ring large-commutative-ring-ℝ ## Properties +### The power operation preserves similarity + +```agda +abstract + preserves-sim-power-ℝ : + {l1 l2 : Level} (n : ℕ) {x : ℝ l1} {y : ℝ l2} → sim-ℝ x y → + sim-ℝ (power-ℝ n x) (power-ℝ n y) + preserves-sim-power-ℝ n = + preserves-sim-power-Large-Commutative-Ring large-commutative-ring-ℝ n _ _ +``` + +### The power operation commutes with raising universe level + +```agda +abstract + power-raise-ℝ : + {l0 : Level} (l : Level) (n : ℕ) (x : ℝ l0) → + power-ℝ n (raise-ℝ l x) ＝ raise-ℝ l (power-ℝ n x) + power-raise-ℝ l n x = + eq-sim-ℝ + ( similarity-reasoning-ℝ + power-ℝ n (raise-ℝ l x) + ~ℝ power-ℝ n x + by preserves-sim-power-ℝ n (sim-raise-ℝ' l x) + ~ℝ raise-ℝ l (power-ℝ n x) + by sim-raise-ℝ l _) +``` + ### The canonical embedding of rational numbers preserves powers ```agda @@ -88,6 +125,13 @@ abstract ( hom-ring-real-ℚ) ( n) ( q)) + + raise-power-real-ℚ : + (l : Level) (n : ℕ) (q : ℚ) → + power-ℝ n (raise-real-ℚ l q) ＝ raise-real-ℚ l (power-ℚ n q) + raise-power-real-ℚ l n q = + ( power-raise-ℝ l n (real-ℚ q)) ∙ + ( ap (raise-ℝ l) (power-real-ℚ n q)) ``` ### `1ⁿ ＝ 1` @@ -431,3 +475,111 @@ abstract ≤ real-ℚ⁺ (power-ℚ⁺ n ε⁺) by leq-eq-ℝ (ap real-ℚ (power-rational-ℚ⁺ n ε⁺))) ``` + +### For any `n`, `power-ℝ n` is pointwise continuous + +```agda +abstract + is-pointwise-continuous-power-ℝ : + {l : Level} (n : ℕ) → is-pointwise-continuous-map-ℝ {l} (power-ℝ n) + is-pointwise-continuous-power-ℝ 0 = + is-pointwise-continuous-const-Metric-Space _ _ _ + is-pointwise-continuous-power-ℝ 1 = + is-pointwise-continuous-map-id-Metric-Space _ + is-pointwise-continuous-power-ℝ {l} (succ-ℕ n@(succ-ℕ _)) = + is-pointwise-continuous-map-comp-pointwise-continuous-map-Metric-Space + ( metric-space-ℝ l) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( metric-space-ℝ l) + ( ind-Σ mul-ℝ , is-pointwise-continuous-mul-ℝ l l) + ( comp-pointwise-continuous-map-Metric-Space + ( metric-space-ℝ l) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( pointwise-continuous-map-product-Metric-Space + ( metric-space-ℝ l) + ( metric-space-ℝ l) + ( metric-space-ℝ l) + ( metric-space-ℝ l) + ( power-ℝ n , is-pointwise-continuous-power-ℝ n) + ( id-pointwise-continuous-map-Metric-Space (metric-space-ℝ l))) + ( pointwise-continuous-isometry-Metric-Space + ( metric-space-ℝ l) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( diagonal-product-isometry-Metric-Space (metric-space-ℝ l)))) + +pointwise-continuous-map-power-ℝ : + (l : Level) (n : ℕ) → pointwise-continuous-map-ℝ l l +pointwise-continuous-map-power-ℝ l n = + ( power-ℝ n , is-pointwise-continuous-power-ℝ n) +``` + +### Odd powers of real numbers preserve strict inequality + +```agda +abstract + is-strictly-increasing-power-is-odd-ℝ : + (l : Level) (n : ℕ) → is-odd-ℕ n → + is-strictly-increasing-function-ℝ (power-ℝ {l} n) + is-strictly-increasing-power-is-odd-ℝ l n odd-n = + is-strictly-increasing-is-strictly-increasing-rational-ℝ + ( pointwise-continuous-map-power-ℝ l n) + ( λ p q pImports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.propositional-truncations +open import foundation.raising-universe-levels +open import foundation.universe-levels + +open import metric-spaces.dense-subsets-metric-spaces + +open import real-numbers.arithmetically-located-dedekind-cuts +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.rational-real-numbers +``` + + + +## Idea + +A +{{#concept "rational approximate" Disambiguation="of a real number" Agda=rational-approximate-ℝ}} +of a [real number](real-numbers.dedekind-real-numbers.md) `x` to some +[positive rational](elementary-number-theory.positive-rational-numbers.md) `ε` +is a [rational number](elementary-number-theory.rational-numbers.md) whose +[canonical embedding](real-numbers.rational-real-numbers.md) in the real numbers +is within an `ε`-neighborhood of `x` in the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). + +## Definition + +```agda +rational-approximate-ℝ : {l : Level} → ℝ l → ℚ⁺ → UU l +rational-approximate-ℝ {l} x ε = + Σ ℚ (λ q → neighborhood-ℝ l ε x (raise-real-ℚ l q)) +``` + +## Properties + +### Any real number can be approximated to any positive rational `ε` + +```agda +abstract opaque + unfolding neighborhood-ℝ real-ℚ + + exists-rational-approximate-ℝ : + {l : Level} (x : ℝ l) (ε : ℚ⁺) → + exists ℚ (λ q → neighborhood-prop-ℝ l ε x (raise-real-ℚ l q)) + exists-rational-approximate-ℝ {l} x ε⁺@(ε , _) = + let + open + do-syntax-trunc-Prop + ( ∃ ℚ (λ q → neighborhood-prop-ℝ l ε⁺ x (raise-real-ℚ l q))) + in do + ((p , q) , qImports + +```agda +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.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.universe-levels + +open import order-theory.strict-order-preserving-maps +open import order-theory.subtypes-strict-preorders + +open import real-numbers.dedekind-real-numbers +open import real-numbers.dense-subsets-real-numbers +open import real-numbers.increasing-functions-real-numbers +open import real-numbers.pointwise-continuous-functions-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.subsets-real-numbers +``` + + + +## Idea + +A function `f` from the [real numbers](real-numbers.dedekind-real-numbers.md) to +themselves is +{{#concept "strictly increasing" Disambiguation="function from ℝ to ℝ" Agda=is-strictly-increasing-function-ℝ}} +if for all `x < y`, `f x < f y`. + +Several arguments on this page are due to +[Mark Saving](https://math.stackexchange.com/users/798694/mark-saving) in this +Mathematics Stack Exchange answer: . + +## Definition + +```agda +is-strictly-increasing-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → Prop (lsuc l1 ⊔ l2) +is-strictly-increasing-prop-function-ℝ {l1} {l2} = + preserves-strict-order-prop-map-Strict-Preorder + ( strict-preorder-ℝ l1) + ( strict-preorder-ℝ l2) + +is-strictly-increasing-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → UU (lsuc l1 ⊔ l2) +is-strictly-increasing-function-ℝ f = + type-Prop (is-strictly-increasing-prop-function-ℝ f) + +is-strictly-increasing-on-subset-function-ℝ : + {l1 l2 l3 : Level} → (ℝ l1 → ℝ l2) → subset-ℝ l3 l1 → UU (lsuc l1 ⊔ l2 ⊔ l3) +is-strictly-increasing-on-subset-function-ℝ {l1} {l2} f S = + preserves-strict-order-map-Strict-Preorder + ( strict-preorder-subtype-Strict-Preorder (strict-preorder-ℝ l1) S) + ( strict-preorder-ℝ l2) + ( f ∘ inclusion-subset-ℝ S) +``` + +## Properties + +### A strictly increasing function is increasing + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + abstract + is-increasing-is-strictly-increasing-function-ℝ : + is-strictly-increasing-function-ℝ f → is-increasing-function-ℝ f + is-increasing-is-strictly-increasing-function-ℝ H = + is-increasing-is-increasing-on-strict-inequalities-ℝ + ( f) + ( λ x y x