normed module identity convergence lemmas - #2029
Conversation
| Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F). | ||
| Proof. by rewrite addrC; apply: is_cvgDlE. Qed. | ||
|
|
||
| Lemma cvgDl f a b : f @ F --> b -> a + f x @[x --> F] --> a + b. |
There was a problem hiding this comment.
What about cvgcstD to suggest that the constant is on the left (and cvgDcst instead of cvgDr)?
Because cvgDl does not really say what is on the left.
But in fact I am not sure that cvgDl, cvgDr, cvgBl, cvgBr are very useful,
because it is just cvg{D,B} with cvg_cst.
The application of cvg_cst should maybe be automatic instead
(and maybe it was thought as such because there is actually a Hint in topology_structure.v but it is not working here). Fixing the latter Hint could be better.
There was a problem hiding this comment.
Yes, I think that would be a better idea; I did find it a bit odd that cvg_cst didn't trigger automatically.
There was a problem hiding this comment.
So now cvg_cst and is_cvg_cst are true hints, this PR can maybe be simplified.
2 participants
Motivation for this change
Split from #2023. Adds convenient
cvglemmas that involves the additive and multiplicative identities of normed modules.Checklist
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