Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Compactum_to_CompHaus.ess_surj

Modification history

2020-12-15 10:30
src/topology/category/Compactum.lean
chore(category_theory/equivalence): weaken essential surjectivity (#3821) …
Added Compactum_to_CompHaus.ess_surjView on Github →