Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-24 00:26 9b1f0bb6

View on Github →

feat(topology/compact_open): convergence in the compact-open topology can be checked on compact sets (#9240)

Estimated changes

Modified src/topology/compact_open.lean

added theorem continuous_map.compact_open_le_induced

added theorem continuous_map.continuous_ev₁

added theorem continuous_map.continuous_restrict

added theorem continuous_map.exists_tendsto_compact_open_iff_forall

added theorem continuous_map.tendsto_compact_open_restrict