Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-25 09:01 6ea81683

View on Github →

refactor(topology/compact_open): use bundled continuous maps (#9351)

Estimated changes

Modified src/topology/compact_open.lean

added theorem continuous_map.continuous_comp

deleted theorem continuous_map.continuous_induced

deleted def continuous_map.induced