Indization

Statistics

Metric	Count
Definitions	0
Theorems `isSeparating_range_yoneda`, `isSeparator_range_yoneda`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isSeparating_range_yoneda` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsSeparating` `CategoryTheory.Ind` `CategoryTheory.instCategoryInd` `CategoryTheory.ObjectProperty.ofObj` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `yoneda`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `CategoryTheory.instHasFilteredColimitsInd` `CategoryTheory.Limits.IndObjectPresentation.instIsFilteredI` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.colimit.hom_ext`
`isSeparator_range_yoneda` 📖	mathematical	—	`CategoryTheory.IsSeparator` `CategoryTheory.Ind` `CategoryTheory.instCategoryInd` `CategoryTheory.Limits.sigmaObj` `CategoryTheory.Functor.obj` `yoneda` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.instHasCoproductsIndOfHasFiniteCoproducts` `CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits` `CategoryTheory.Discrete.functor`	—	`CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.instHasCoproductsIndOfHasFiniteCoproducts` `CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits` `isSeparating_range_yoneda`

---