Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_map.equiv_fn_of_discrete

Modification history

2021-03-17 01:14
src/topology/continuous_map.lean
feat(topology/continuous_map): lattice structures (#6706)
Added continuous_map.equiv_fn_of_discreteView on Github →