ExtensiveTopology

Statistics

Metric	Count
Definitions	0
Theorems `mem_sieves_iff_contains_colimit_cofan`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_sieves_iff_contains_colimit_cofan` 📖	mathematical	—	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.extensiveTopology` `CategoryTheory.Limits.IsColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.Sieve.arrows`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts` `CategoryTheory.Category.id_comp` `Finite.of_fintype` `CategoryTheory.Limits.hasColimit_of_domain_hasInitial` `CategoryTheory.Limits.HasZeroObject.hasInitial` `CategoryTheory.Limits.hasZeroObject_pUnit` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.Limits.hasCoproduct_unique` `Unique.instSubsingleton` `CategoryTheory.Iso.isIso_hom` `Finite.instSigma` `CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset` `CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc`

---