Theorem UniformFun.isClosed_setOf_continuous

Modification history

2026-07-17 09:57

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Deleted UniformFun.isClosed_setOf_continuous View on Github →

2024-03-08 16:17

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

feat(UniformConvergenceTopology): add `isClosed_setOf_continuous` (#10902) …

Added UniformFun.isClosed_setOf_continuous View on Github →