[Merged by Bors] - feat(topology/compact_open): convergence in the compact-open topology can be checked on compact sets #9240
Conversation
hrmacbeth
commented
Sep 17, 2021
•
hrmacbeth
commented
- depends on: [Merged by Bors] - feat(topology/continuous_function/basic): gluing lemmas #9239
hrmacbeth
added
the
awaiting-review
github-actions
bot
added
blocked-by-other-PR
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
| lemma exists_tendsto_compact_open_iff_forall [locally_compact_space α] [t2_space α] [t2_space β] | ||
| {ι : Type*} {l : filter ι} [filter.ne_bot l] (F : ι → C(α, β)) : | ||
| (∃ f, filter.tendsto F l (𝓝 f)) | ||
| ↔ ∀ (s : set α) (hs : is_compact s), ∃ f, filter.tendsto (λ i, (F i).restrict s) l (𝓝 f) := |
There was a problem hiding this comment.
Would it be useful to the end-user if there were companion lemmas that say "those fs for each s are the restriction of f to each s" and in the other direction "and all these fs can be glued together, obtaining a function to which F converges"?
No problem if you think either "it wouldn't be that useful" or "it can happen later"!
There was a problem hiding this comment.
I've added a couple of more general lemmas which imply this information: (1) if a family F converges to f, then the restrictions of F to s converge to the restriction of f to s; (2) under appropriate hypotheses continuous_map is a Hausdorff space (hence, limits are unique). I think these are useful so thanks for prompting this!
There was a problem hiding this comment.
I'd be tempted to have the explicit lemmas in both directions, to be sure we really have the API available, but I can see the argument that the explicit lemmas might not often be needed. I'll hit bors d+ now, but do feel free to add more if you like! :-)
There was a problem hiding this comment.
Oh! My instinct is the opposite, that the gluing construction lift_cover_restrict' is an implementation detail for which it's better to expose only certain carefully selected properties :-). I'll take your bors d+ for now, but I expect that when @CBirkbeck and others start using this construction heavily, we'll find out what's best.
|
bors d+ |
|
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
… can be checked on compact sets (#9240)
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
