Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_map.coe_coe

Modification history

2022-09-30 06:01
src/topology/continuous_function/basic.lean
feat(topology/continuous_function/{basic, compact}): add a few missing lemmas (#16714)
Added continuous_map.coe_coeView on Github →