Def CocompactMapClass.toCocompactMap

Modification history

2023-08-19 12:28
Mathlib/Topology/ContinuousFunction/CocompactMap.lean
chore: make sure that some coercions have an attached definition (#6667)
Added CocompactMapClass.toCocompactMapView on Github →