Commit 2024-03-08 16:17 cb921c1c

View on Github →

feat(UniformConvergenceTopology): add isClosed_setOf_continuous (#10902) See Zulip chat

Estimated changes

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

added theorem UniformFun.isClosed_setOf_continuous

added theorem UniformOnFun.isClosed_setOf_continuous_of_le