mathlib

b6258037 - feat(topology/uniform_space/uniform_convergence): tendsto_uniformly_on_filter (#15871)

feat(topology/uniform_space/uniform_convergence): tendsto_uniformly_on_filter (#15871) Currently, mathlib supports several notions of uniform convergence (e.g., tendsto_uniformly_on). These are "global" versions of a more local notion, which we call tendsto_uniformly_on_filter. Specifically, as revealed by tendsto_prod_top_iff is that uniform convergence means convergence on a product filter. So why can't you have a more general filter than a principal filter? There's no reason you can't! Indeed, if you replace 𝓟 s with 𝓝 x you get a notion of "local uniform convergence" which is enough to prove, e.g., the derivative operator at a point commutes with the pointwise limit.