Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-24 21:31 6434658c

View on Github →

feat(analysis/topology): locally compact spaces and the compact-open topology

Estimated changes

Created analysis/topology/compact_open.lean

added def coev

added def compact_open

added def compact_open_gen

added theorem continuous_coev

added theorem continuous_ev

added theorem continuous_induced

added def continuous_map.induced

added def ev

added theorem image_coev

added theorem locally_compact_of_compact

added theorem locally_compact_of_compact_nhds

Modified analysis/topology/topological_space.lean

added theorem compact_diff

added theorem compact_inter