Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-01 14:40 b66614d1

View on Github →

refactor(analysis/topology): renamed compact_open to continuous_map; moved locally_compact to a more general position

Estimated changes

Modified analysis/topology/continuity.lean

added theorem locally_compact_of_compact

added theorem locally_compact_of_compact_nhds

Renamed analysis/topology/compact_open.lean to analysis/topology/continuous_map.lean

deleted def coev

deleted def compact_open

deleted def compact_open_gen

deleted theorem continuous_coev

deleted theorem continuous_ev

deleted theorem continuous_induced

added def continuous_map.coev

added def continuous_map.compact_open.gen

added theorem continuous_map.continuous_coev

added theorem continuous_map.continuous_ev

added theorem continuous_map.continuous_induced

added def continuous_map.ev

added theorem continuous_map.image_coev

modified def continuous_map.induced

added def continuous_map

deleted def ev

deleted theorem image_coev

deleted theorem locally_compact_of_compact

deleted theorem locally_compact_of_compact_nhds