Commit 2024-05-08 01:12 628b2666

View on Github →

feat(UniformConvergenceTopology): prove CompleteSpace (#10844)

Estimated changes

Modified Mathlib/Topology/UniformSpace/Equiv.lean

modified theorem UniformEquiv.comap_eq

added theorem UniformEquiv.completeSpace_iff

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

added theorem UniformOnFun.uniformContinuous_eval_of_mem_sUnion

added theorem UniformOnFun.uniformContinuous_ofUniformFun

added def UniformOnFun.uniformEquivUniformFun