Topologies of uniform convergence on sets

Stream: general

[Anatole Dedecker]

In #13073 I introduced the uniform structures on X → Y of uniform convergence, first on X as a whole, and then on a family of subsets of X. However, there are two main problems with the setup I introduced :

• we must have annoying @s everywhere, because we can't make this an instance. For the "convergence on X" case we can of course replace Pi.uniform_space with uniform_convergence.uniform_space locally, but we can't even do that for convergence on a family of subsets, because the family of subsets has to be an explicit parameter. The only solution I see is introducing a type alias, but I'm not sure it would be really worth it : if I understand well, you rarely want to put such a topology on bare functions, but I lack experience, is this true ?
• most lemmas have both a "convergence on X" and "convergence on some subsets" form. This might not be obvious for what is currently in mathlib, but you can have a look at #14534 for good examples of this. The way I deal with this is by having two namespaces uniform_convergence and uniform_convergence_on and making every possible conflicting lemma protected, but that means working with annoyingly long names everywhere. @Patrick Massot suggested working only with the "convergence on subsets" definition and using the family {univ} (or (univ : set X), this gives the same topology) by default (which, if I understand correctly, means creating a tactic like of docs#measure_theory.volume_tac ). But I think it makes it impossible to declare it as a local instance, even in the global case ?? (or at least I don't know how to do it without putting a separate definition for the global case). And finally, since the "convergence on subsets" uniformity is defined in terms of the global one, that also means having a bunch of things about an auxiliary definitions just to translate them to the one we actually use. I'll definitely try this option to see if it works better, but it doesn't seem ideal, does anyone have other suggestions about this ?

Thanks !