isolate the theory of lime_sup #1121
Conversation
affeldt-aist
added
enhancement ✨
|
What about adding these (loosely related) lemmas https://github.com/zstone1/analysis/blob/total_variation/theories/realfun.v#L1323-L1352 |
at least related to this one https://github.com/affeldt-aist/analysis/blob/limr_sup/theories/realfun.v#L88-L105 |
There was a problem hiding this comment.
The repeated proofs about swapping between sequential and filter convergence are annoying, but tough to fix without a little extra machinery.
The interesting question is about generalizing this to consider the lim_sup of a function "at a filter". If it's an easy generalization, we should do it now. If it's tough, then we may have to revisit the material when we do sequence limsups.
| Section cvgr_fun_cvg_seq. | ||
| Context {R : realType}. | ||
|
|
||
| Lemma cvg_at_rightP (f : R -> R) (p l : R) : |
There was a problem hiding this comment.
In a textbook all four of these proofs would be three liners:
- In first countable spaces, filter convergence <-> sequence convergence
- The lower (upper) limit topology (AKA sogenfrey line) is first countable
- All sequences in the lower (upper) limit topology that converge, do so from the left (right).
The proof you have is fine, I'm not complaining about it. I am complaining that some missing classical machinery is making these proofs longer than necessary. A problem for another day, I guess.
Co-authored-by: Zachary Stone <[email protected]>
* isolate the theory of lime_sup - generic def of limsup --------- Co-authored-by: Zachary Stone <[email protected]>
* isolate the theory of lime_sup - generic def of limsup --------- Co-authored-by: Zachary Stone <[email protected]>
proux01
removed
the
TODO: MC2 port
Motivation for this change
from the PR #1065 on the Lebesgue differentiation theorem
Things done/to do
CHANGELOG_UNRELEASED.mdCompatibility with MathComp 2.0
TODO: HB portto make sure someone ports this PR tothe
hierarchy-builderbranch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.