Theorem UniformOnFun.isClosed_setOf_continuous

Modification history

2025-04-09 06:03

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

chore: rename `RestrictGenTopology` to `Topology.IsCoherentWith` (#18397) …

Modified UniformOnFun.isClosed_setOf_continuous View on Github →

2024-06-29 22:58

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

feat: define `RestrictGenTopology` (#13452)

Added UniformOnFun.isClosed_setOf_continuous View on Github →