Mathlib Changelog
v3
Changelog
About
Github
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