[Merged by Bors] - feat(UniformConvergenceTopology): add UniformOnFun.uniformity_eq etc

[urkud]

• Add UniformOnFun.uniformity_eq etc:
  the HasBasis statements need more assumptions.
• Add missing toFun/ofFun.
• Golf using new lemmas.

---

[urkud]

I made the proof much shorter. Should I restore some of the comments?

[ADedecker]

TBH I'm a bit sad to see my proof go, mostly because I like this kind of argument, but I have no objective argument for keeping it (I suggested a slight golf though). As for comments, I'd say you could just add the following at the beginning of the proof, to match more accurately the new version:

  -- This follows from the fact that `(— ∘ f) × (— ∘ f)` maps `gen (f '' t) V` to `gen t V`.

[ADedecker]

Thanks and sorry for the delay.

bors d+

[ADedecker]

TBH I'm a bit sad to see my proof go, mostly because I like this kind of argument, but I have no objective argument for keeping it (I suggested a slight golf though). As for comments, I'd say you could just add the following at the beginning of the proof, to match more accurately the new version:

  -- This follows from the fact that `(— ∘ f) × (— ∘ f)` maps `gen (f '' t) V` to `gen t V`.

[mathlib-bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[leanprover-community-mathlib4-bot]

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style