[Merged by Bors] - refactor(UniformConvergenceTopology): redefine using UniformOnFun
#10873
Conversation
urkud
commented
Feb 23, 2024
•
urkud
commented
- TODO: fix module docs
urkud
added
awaiting-review
awaiting-CI
t-topology
There was a problem hiding this comment.
This is great, it's been in the back of my mind for ages so I'm glad it's now happening.
The module doc string does deserve some careful attention since for example the Main definitions / results section is now out of date. On the other hand, the first two sections Compact convergence (uniform convergence on compact sets) and The uniform space structure still look useful. Perhaps we could keep these and explain in the Implementation details section that we now factor through the more general theory.
Apart from this and the nitpicks below everything looks good. I am also happy to let you make the call on the doc string (including if you disagree with my remarks above, and decided to excise / rewrite it).
bors d+
| refine eq_of_nhds_eq_nhds fun f ↦ eq_of_forall_le_iff fun l ↦ ?_ | ||
| simp_rw [← tendsto_id', tendsto_iff_forall_compact_tendstoUniformlyOn, | ||
| nhds_induced, tendsto_comap_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn] | ||
| rfl |
There was a problem hiding this comment.
Or if you prefer:
| rfl | |
| exact forall₄_congr fun U _ hU _ ↦ by simp |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Oliver Nash <github@olivernash.org>
|
I'll updates the docs later. |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
UniformOnFunUniformOnFun
|
Ooooooh I missed that (I was preparing for an exam...), thanks a lot! |
