Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_map.nhds_compact_open_eq_Inf_nhds_induced

Modification history

2021-09-10 16:18
src/topology/compact_open.lean
feat(topology/compact_open): express the compact-open topology as an Inf of topologies (#9106) …
Added continuous_map.nhds_compact_open_eq_Inf_nhds_inducedView on Github →