Commit 2023-02-24 03:17 b305fd4d

View on Github →

feat: port Topology.UniformSpace.UniformConvergenceTopology (#2159)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

added def UniformFun.ofFun

added def UniformFun.toFun

added theorem UniformFun.uniformContinuous_eval

added def UniformFun

added def UniformOnFun.ofFun

added theorem UniformOnFun.t2Space_of_covering

added def UniformOnFun.toFun

added theorem UniformOnFun.uniformContinuous_eval_of_mem

added def UniformOnFun