Odd powers of real numbers are strictly increasing #1737
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-authored-by: Fredrik Bakke <[email protected]>
Co-authored-by: Fredrik Bakke <[email protected]>
Co-authored-by: Fredrik Bakke <[email protected]>
Co-authored-by: Fredrik Bakke <[email protected]>
Co-authored-by: Fredrik Bakke <[email protected]>
src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/classically-pointwise-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/classically-pointwise-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/classical-limits-of-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/classical-limits-of-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/classical-limits-of-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
Co-authored-by: Fredrik Bakke <[email protected]>
| ( f) | ||
| ( is-uniformly-continuous-is-short-function-Metric-Space X Y f H) | ||
|
|
||
| pointwise-continuous-short-function-Metric-Space : |
Collaborator
There was a problem hiding this comment.
Suggested change
| pointwise-continuous-short-function-Metric-Space : | |
| pointwise-continuous-map-short-function-Metric-Space : |
| where | ||
|
|
||
| abstract | ||
| is-pointwise-continuous-const-Metric-Space : |
Collaborator
There was a problem hiding this comment.
Suggested change
| is-pointwise-continuous-const-Metric-Space : | |
| is-pointwise-continuous-map-const-Metric-Space : |
| where | ||
|
|
||
| abstract | ||
| is-pointwise-continuous-is-isometry-Metric-Space : |
Collaborator
There was a problem hiding this comment.
Suggested change
| is-pointwise-continuous-is-isometry-Metric-Space : | |
| is-pointwise-continuous-map-is-isometry-Metric-Space : |
| 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 : |
Collaborator
There was a problem hiding this comment.
Suggested change
| pointwise-continuous-uniformly-continuous-function-Metric-Space : | |
| pointwise-continuous-map-uniformly-continuous-function-Metric-Space : |
| where | ||
|
|
||
| abstract | ||
| is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space : |
Collaborator
There was a problem hiding this comment.
Suggested change
| is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space : | |
| is-pointwise-continuous-map-is-uniformly-continuous-function-Metric-Space : |
| ( f) | ||
| ( is-uniformly-continuous-is-isometry-Metric-Space X Y f H) | ||
|
|
||
| pointwise-continuous-isometry-Metric-Space : |
Collaborator
There was a problem hiding this comment.
Suggested change
| pointwise-continuous-isometry-Metric-Space : | |
| pointwise-continuous-map-isometry-Metric-Space : |
Collaborator
There was a problem hiding this comment.
The convention in order-theory is to call a subtype of an ordering a subordering, i.e., here, `Strict-Subpreorder. Are you intentionally going against that convention? C.f. for instance subpreorders.
Comment on lines
+61
to
+62
| is-classical-limit-is-limit-function-ℝ : | ||
| is-limit-function-ℝ f x y → is-classical-limit-function-ℝ f x y |
Collaborator
There was a problem hiding this comment.
Here the terminology map should also be preferred over function and for the rest of this file. If you prefer, I'm willing to postpone the renaming to a dedicated PR.
Comment on lines
+42
to
+43
| is-classically-pointwise-continuous-prop-function-ℝ : Prop (lsuc l1 ⊔ l2) | ||
| is-classically-pointwise-continuous-prop-function-ℝ = |
Collaborator
There was a problem hiding this comment.
Here and for the rest of this file also map should be preferred over function. Again I'm open to postpone renamings for a dedicated PR.
Comment on lines
+68
to
+74
| 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) |
Comment on lines
+33
to
+42
| 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) |
Comment on lines
+41
to
+46
| 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) |
Collaborator
There was a problem hiding this comment.
same here and for the rest of this file
Comment on lines
+704
to
+719
| abstract | ||
| extensionality-principle-strict-preorder-ℝ : | ||
| (l : Level) → | ||
| extensionality-principle-Strict-Preorder (strict-preorder-ℝ l) | ||
| extensionality-principle-strict-preorder-ℝ l x y (_ , x~y) = | ||
| eq-sim-ℝ | ||
| ( sim-le-same-rational-ℝ x y | ||
| ( λ q → | ||
| ( inv-iff (le-iff-le-right-raise-ℝ l y (real-ℚ q))) ∘iff | ||
| ( x~y (raise-real-ℚ l q)) ∘iff | ||
| ( le-iff-le-right-raise-ℝ l x (real-ℚ q)))) | ||
|
|
||
| strict-order-ℝ : (l : Level) → Strict-Order (lsuc l) l | ||
| strict-order-ℝ l = | ||
| ( strict-preorder-ℝ l , | ||
| extensionality-principle-strict-preorder-ℝ l) |
Collaborator
There was a problem hiding this comment.
Oh, nice, it's good to know that this extensionality principle is sensible!
Collaborator
|
This PR has gotten very large, and I think it needs a proper re-review before I'm confident to merge it. Would it be possible to split it up into a few smaller PRs? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Builds on some material from #1712 .