# mathlibdocumentation

topology.category.Top.epi_mono

# Epi- and monomorphisms in Top#

This file shows that a continuous function is an epimorphism in the category of topological spaces if and only if it is surjective, and that a continuous function is a monomorphism in the category of topological spaces if and only if it is injective.

theorem Top.epi_iff_surjective {X Y : Top} (f : X Y) :
theorem Top.mono_iff_injective {X Y : Top} (f : X Y) :