Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_map.ev

Modification history

2022-03-17 11:06
src/topology/compact_open.lean
chore(topology/compact_open): remove `continuous_map.ev`, and rename related lemmas to `eval'` (#12738) …
Deleted continuous_map.evView on Github →
2018-10-01 14:40
analysis/topology/continuous_map.lean
refactor(analysis/topology): renamed compact_open to continuous_map; moved locally_compact to a more general position
Added continuous_map.evView on Github →