Set

📁 Source: Mathlib/CategoryTheory/Limits/Set.lean

Statistics

Metric	Count
Definitions	0
Theorems instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty	1
Total	1

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape Set Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra CategoryTheory.types functorToTypes	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone

---

← Back to Index