Commit 2024-07-02 02:03 d1415c6a

View on Github →

feat(UniformConvergenceTopology): prove generic UniformOnFun.continuousOn_eval₂ (#13532) Also use it to weaken TC assumptions in ContinuousMultilinearMap.continuous_eval.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

modified theorem ContinuousMultilinearMap.continuous_eval

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean