Nonempty

📁 Source: Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean

Statistics

Metric	Count
Definitions mkOfBot, mkOfLimit, functor, inductiveSystem, mkOfSucc	5
Theorems arrowMap_functor, arrowMap_functor_to_top, functor_obj, inductiveSystem_map, inductiveSystem_obj, nonempty	6
Total	11

CategoryTheory.SmallObject.SuccStruct.Iteration

Definitions

Name	Category	Theorems
mkOfBot 📖	CompOp	—
mkOfLimit 📖	CompOp	—
mkOfSucc 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty 📖	mathematical	—	CategoryTheory.SmallObject.SuccStruct.Iteration	—	—

CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit

Definitions

Name	Category	Theorems
functor 📖	CompOp	3 math math: arrowMap_functor, functor_obj, arrowMap_functor_to_top
inductiveSystem 📖	CompOp	3 math math: inductiveSystem_obj, inductiveSystem_map, arrowMap_functor_to_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowMap_functor 📖	mathematical	Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE Preorder.toLT	CategoryTheory.SmallObject.SuccStruct.arrowMap functor LT.lt.le CategoryTheory.Functor.obj Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership CategoryTheory.SmallObject.SuccStruct.Iteration.F lt_of_le_of_lt CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj	—	CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone
arrowMap_functor_to_top 📖	mathematical	Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	CategoryTheory.SmallObject.SuccStruct.arrowMap functor LT.lt.le CategoryTheory.Functor.obj Set.Elem Set.Iio Preorder.smallCategory Subtype.preorder Set Set.instMembership inductiveSystem CategoryTheory.Limits.colimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit CategoryTheory.Limits.colimit.ι	—	CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top
functor_obj 📖	mathematical	Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Preorder.toLE	CategoryTheory.Functor.obj Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership functor LT.lt.le CategoryTheory.SmallObject.SuccStruct.Iteration.F	—	LT.lt.le CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj
inductiveSystem_map 📖	mathematical	—	CategoryTheory.Functor.map Set.Elem Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.smallCategory Subtype.preorder Set Set.instMembership inductiveSystem CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj	—	—
inductiveSystem_obj 📖	mathematical	—	CategoryTheory.Functor.obj Set.Elem Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.smallCategory Subtype.preorder Set Set.instMembership inductiveSystem Set.Iic CategoryTheory.SmallObject.SuccStruct.Iteration.F	—	—

---

← Back to Index