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 TopCat.epi_iff_surjective {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem TopCat.mono_iff_injective {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)