Mathlib v3 is deprecated. Go to Mathlib v4

Def Compactum_to_CompHaus_comp_forget

Modification history

2022-01-28 03:07
src/topology/category/Compactum.lean
feat(topology/category/Compactum): forget creates limits (#11690) …
Added Compactum_to_CompHaus_comp_forgetView on Github →