mathlib documentation

topology.category.Top.epi_mono

source
theorem Top.epi_iff_surjective {X Y : Top} (f : X ⟶ Y) :
category_theory.epi f ↔ function.surjective ⇑f

source
theorem Top.mono_iff_injective {X Y : Top} (f : X ⟶ Y) :
category_theory.mono f ↔ function.injective ⇑f