This repository was archived by the owner on Jul 24, 2024. It is now read-only.
feat(analysis/normed_space/deriv): show that the differential is unique#830
Closed
jdsalchow wants to merge 10 commits intoleanprover-community:masterfrom
Closed
feat(analysis/normed_space/deriv): show that the differential is unique#830jdsalchow wants to merge 10 commits intoleanprover-community:masterfrom
jdsalchow wants to merge 10 commits intoleanprover-community:masterfrom
Conversation
sgouezel
reviewed
Mar 17, 2019
|
|
||
| /-- The differential of a map at a point along a filter is unique, given that filter is coarser than the | ||
| neighbourhood filter of the point.-/ | ||
| lemma fderiv_at_filter_unique (f : E → F) (x₀ : E) {L : filter E} (h : nhds x₀ ≤ L) {A₁ A₂ : E → F} : |
Collaborator
There was a problem hiding this comment.
Is there a way to make sure that the beginning and end of the proof are clearly identified? You are following mathlib style, sure, but I feel it is confusing. Maybe avoid blank lines in the middle of the proof (just adding -- on a blank line would help), and adding --end of proof at the end?
sgouezel
reviewed
Mar 17, 2019
1f77b9e to
2d04a6c
Compare
avigad
previously requested changes
Apr 6, 2019
sgouezel
reviewed
Apr 9, 2019
Collaborator
|
Could you remove the empty lines in the proof of |
sgouezel
reviewed
Apr 9, 2019
Collaborator
Author
|
I would re-PR this as from a branch on |
Collaborator
Author
|
I've re-PRd this as #916. |
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
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
3 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.
Show that the differential at a point is unique, if it is taken along a filter finer than the neighbourhood filter at the point.
This depends on #829 .
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list