Utility lemmas in filter.v - #2024
Conversation
573976b to
5741664
Compare
| {near F, f =1 g} -> lim (f @ F) = lim (g @ F). | ||
| Proof. by move=> /near_eq_cvgE ->. Qed. | ||
|
|
||
| Lemma cvg_to_eq {T : nbhsType} {F : set_system T} (l l' : T) : |
There was a problem hiding this comment.
That does not look very useful a priori.
There was a problem hiding this comment.
I found it useful in cases where the convergence is easy to close out with lemmas like cvgD, cvgM with an existential as the target, but where the end result needs some rewriting to be shown equal to the desired quantity, somewhat like is_derive_eq.
There was a problem hiding this comment.
I think that is_derive_eq comes with typeclass instances so that when it is applied, it returns only one goal (the equality). Maybe this is a difference with cvg_to_eq?
There was a problem hiding this comment.
What about we remove this lemma from this PR and defer its inclusion to a PR that actually uses it? (That would unlock this PR because the other lemmas looks ok to me.)
ad3d294 to
a22136a
Compare
* Utility lemmas in filter.v --------- Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
2 participants
Motivation for this change
Split from #2023
Checklist
added corresponding entries in
CHANGELOG_UNRELEASED.mdadded corresponding documentation in the headersReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers