Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_map.coe_restrict

Modification history

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