[Merged by Bors] - feat: inv lemmas for uniform convergence, missing to_fun attributes#35384

sgouezel wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_isUnifInvsgouezel/mathlib4:SG_isUnifInvCopy head branch name to clipboard