EpiMono

Statistics

Metric	Count
Definitions	0
Theorems `epi_iff_surjective`, `mono_iff_injective`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `TopCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Functor.map_epi` `CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint` `instIsLeftAdjointForgetContinuousMapCarrier` `CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.epi_iff_surjective`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `TopCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Functor.map_mono` `CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint` `instIsRightAdjointForgetContinuousMapCarrier` `CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.mono_iff_injective`

---