Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `SuccStruct`, `Iteration`, `F`, `isColimit`, `mapObj`, `MapEq`, `trunc`, `X₀`, `arrowMap`, `arrowSucc`, `arrowι`, `ofNatTrans`, `prop`, `arrowIso`, `succ`, `toSucc`, `toSuccArrow`, `coconeOfLE`, `restrictionLE`, `restrictionLT`	20
Theorems `arrowMap_limit`, `arrowSucc_eq`, `arrow_mk_mapObj`, `congr_arrowMap`, `congr_map`, `congr_obj`, `ext`, `ext_iff`, `mapObj_refl`, `mapObj_trans`, `mapObj_trans_assoc`, `obj_bot`, `obj_limit`, `obj_succ`, `prop_map_succ`, `subsingleton`, `src`, `tgt`, `w`, `ext`, `mapEq_refl`, `mapEq_trans`, `trunc_F`, `arrowMap_refl`, `arrowMap_restrictionLE`, `arrowSucc_def`, `arrowι_def`, `ofNatTrans_X₀`, `ofNatTrans_succ`, `ofNatTrans_toSucc`, `arrowIso_hom_left`, `arrowIso_hom_right`, `arrowIso_inv_left`, `arrowIso_inv_right`, `fac`, `fac_assoc`, `succ_eq`, `prop_iff`, `prop_toSucc`, `toSuccArrow_hom`, `toSuccArrow_left`, `toSuccArrow_right`, `coconeOfLE_pt`, `coconeOfLE_ι_app`, `restrictionLE_map`, `restrictionLE_obj`, `restrictionLT_map`, `restrictionLT_obj`	48
Total	68

CategoryTheory.SmallObject

Definitions

Name	Category	Theorems
`SuccStruct` 📖	CompData	—
`coconeOfLE` 📖	CompOp	2 math math: `coconeOfLE_pt`, `coconeOfLE_ι_app`
`restrictionLE` 📖	CompOp	6 math math: `SuccStruct.extendToSuccRestrictionLEIso_hom_app`, `restrictionLE_map`, `SuccStruct.extendToSuccRestrictionLEIso_inv_app`, `SuccStruct.arrowMap_restrictionLE`, `SuccStruct.Iteration.trunc_F`, `restrictionLE_obj`
`restrictionLT` 📖	CompOp	8 math math: `SuccStruct.restrictionLTOfCoconeIso_inv_app`, `coconeOfLE_pt`, `SuccStruct.restrictionLTOfCoconeIso_hom_app`, `SuccStruct.Iteration.obj_limit`, `SuccStruct.Iteration.arrowMap_limit`, `restrictionLT_obj`, `restrictionLT_map`, `coconeOfLE_ι_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coconeOfLE_pt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`CategoryTheory.Limits.Cocone.pt` `Set.Elem` `Set.Iio` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `restrictionLT` `coconeOfLE` `CategoryTheory.Functor.obj` `Set.Iic` `Subtype.partialOrder`	—	—
`coconeOfLE_ι_app` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`CategoryTheory.NatTrans.app` `Set.Elem` `Set.Iio` `Preorder.smallCategory` `Subtype.partialOrder` `Set` `Set.instMembership` `CategoryTheory.Functor.comp` `Set.Iic` `Monotone.functor` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `Set.principalSegIioIicOfLE` `PrincipalSeg.monotone` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `PrincipalSeg.top` `CategoryTheory.Limits.Cocone.ι` `Subtype.preorder` `restrictionLT` `coconeOfLE` `CategoryTheory.Functor.map` `LE.le.trans` `LT.lt.le` `CategoryTheory.homOfLE`	—	`PrincipalSeg.monotone`
`restrictionLE_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`CategoryTheory.Functor.map` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `restrictionLE` `CategoryTheory.Functor.obj` `Subtype.partialOrder` `Monotone.functor` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `InitialSeg.instFunLike` `Set.initialSegIicIicOfLE` `CategoryTheory.homOfLE`	—	—
`restrictionLE_obj` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `restrictionLE` `LE.le.trans`	—	—
`restrictionLT_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`CategoryTheory.Functor.map` `Set.Elem` `Set.Iio` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `restrictionLT` `Set.Iic` `CategoryTheory.Functor.obj` `Subtype.partialOrder` `Monotone.functor` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `Set.principalSegIioIicOfLE` `CategoryTheory.homOfLE`	—	—
`restrictionLT_obj` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iio` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `restrictionLT` `Set.Iic` `LE.le.trans` `LT.lt.le`	—	—

CategoryTheory.SmallObject.SuccStruct

Definitions

Name	Category	Theorems
`Iteration` 📖	CompData	2 math math: `Iteration.nonempty`, `Iteration.subsingleton`
`X₀` 📖	CompOp	6 math math: `ofNatTrans_X₀`, `Iteration.obj_bot`, `transfiniteCompositionOfShapeιIteration_isoBot`, `transfiniteCompositionOfShapeιIteration_incl`, `transfiniteCompositionOfShapeιIteration_F`, `transfiniteCompositionOfShapeιIteration_isColimit`
`arrowMap` 📖	CompOp	11 math math: `arrowMap_refl`, `arrowMap_ofCocone_to_top`, `arrowMap_restrictionLE`, `Iteration.congr_arrowMap`, `Iteration.mkOfLimit.arrowMap_functor`, `Iteration.arrowMap_limit`, `arrowMap_ofCocone`, `Iteration.mkOfLimit.arrowMap_functor_to_top`, `arrowSucc_def`, `arrowMap_extendToSucc`, `Iteration.arrow_mk_mapObj`
`arrowSucc` 📖	CompOp	3 math math: `Iteration.arrowSucc_eq`, `arrowSucc_extendToSucc`, `arrowSucc_def`
`arrowι` 📖	CompOp	2 math math: `arrowι_def`, `Iteration.arrowMap_limit`
`ofNatTrans` 📖	CompOp	3 math math: `ofNatTrans_X₀`, `ofNatTrans_succ`, `ofNatTrans_toSucc`
`prop` 📖	CompOp	11 math math: `prop_iff`, `CategoryTheory.SmallObject.succStruct_prop_le_propArrow`, `transfiniteCompositionOfShapeιIteration_isoBot`, `transfiniteCompositionOfShapeιIteration_incl`, `prop_iterationFunctor_map_succ`, `transfiniteCompositionOfShapeιIteration_F`, `prop_toSucc`, `CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration_F`, `CategoryTheory.SmallObject.prop_iterationFunctor_map_succ`, `Iteration.prop_map_succ`, `transfiniteCompositionOfShapeιIteration_isColimit`
`succ` 📖	CompOp	11 math math: `prop.arrowIso_inv_right`, `prop.arrowIso_hom_right`, `iterationFunctor_map_succ_assoc`, `Iteration.obj_succ`, `prop.succ_eq`, `iterationFunctor_map_succ`, `prop.fac_assoc`, `prop.fac`, `toSuccArrow_right`, `prop_toSucc`, `ofNatTrans_succ`
`toSucc` 📖	CompOp	7 math math: `toSuccArrow_hom`, `iterationFunctor_map_succ_assoc`, `iterationFunctor_map_succ`, `prop.fac_assoc`, `prop.fac`, `prop_toSucc`, `ofNatTrans_toSucc`
`toSuccArrow` 📖	CompOp	9 math math: `prop.arrowIso_hom_left`, `prop.arrowIso_inv_left`, `prop_iff`, `prop.arrowIso_inv_right`, `prop.arrowIso_hom_right`, `toSuccArrow_hom`, `Iteration.arrowSucc_eq`, `toSuccArrow_left`, `toSuccArrow_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrowMap_refl` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`arrowMap` `CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Functor.map_id`
`arrowMap_restrictionLE` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`arrowMap` `CategoryTheory.SmallObject.restrictionLE` `LE.le.trans`	—	—
`arrowSucc_def` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`arrowSucc` `arrowMap` `Order.succ` `Order.le_succ` `Order.succ_le_of_lt`	—	—
`arrowι_def` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	`arrowι` `CategoryTheory.Functor.obj` `Set.Elem` `Set.Iio` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `CategoryTheory.Limits.colimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit` `CategoryTheory.Limits.colimit.ι`	—	—
`ofNatTrans_X₀` 📖	mathematical	—	`X₀` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `ofNatTrans` `CategoryTheory.Functor.id`	—	—
`ofNatTrans_succ` 📖	mathematical	—	`succ` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `ofNatTrans` `CategoryTheory.Functor.comp`	—	—
`ofNatTrans_toSucc` 📖	mathematical	—	`toSucc` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `ofNatTrans` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Functor.id`	—	—
`prop_iff` 📖	mathematical	—	`prop` `toSuccArrow`	—	`CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff` `prop_toSucc`
`prop_toSucc` 📖	mathematical	—	`prop` `succ` `toSucc`	—	—
`toSuccArrow_hom` 📖	mathematical	—	`CategoryTheory.Comma.hom` `CategoryTheory.Functor.id` `toSuccArrow` `toSucc`	—	—
`toSuccArrow_left` 📖	mathematical	—	`CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `toSuccArrow`	—	—
`toSuccArrow_right` 📖	mathematical	—	`CategoryTheory.Comma.right` `CategoryTheory.Functor.id` `toSuccArrow` `succ`	—	—

CategoryTheory.SmallObject.SuccStruct.Iteration

Definitions

Name	Category	Theorems
`F` 📖	CompOp	20 math math: `CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map`, `mkOfLimit.inductiveSystem_obj`, `obj_bot`, `congr_obj`, `obj_succ`, `mapObj_trans_assoc`, `arrowSucc_eq`, `mapObj_refl`, `congr_arrowMap`, `mkOfLimit.arrowMap_functor`, `obj_limit`, `arrowMap_limit`, `congr_map`, `trunc_F`, `mkOfLimit.functor_obj`, `ext_iff`, `CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj`, `prop_map_succ`, `mapObj_trans`, `arrow_mk_mapObj`
`isColimit` 📖	CompOp	—
`mapObj` 📖	CompOp	6 math math: `mkOfLimit.inductiveSystem_map`, `mapObj_trans_assoc`, `mapObj_refl`, `mkOfLimit.arrowMap_functor`, `mapObj_trans`, `arrow_mk_mapObj`
`trunc` 📖	CompOp	1 math math: `trunc_F`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrowMap_limit` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `Preorder.toLT`	`CategoryTheory.SmallObject.SuccStruct.arrowMap` `F` `LT.lt.le` `CategoryTheory.SmallObject.SuccStruct.arrowι` `CategoryTheory.SmallObject.restrictionLT`	—	—
`arrowSucc_eq` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.SmallObject.SuccStruct.arrowSucc` `F` `CategoryTheory.SmallObject.SuccStruct.toSuccArrow` `CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `LT.lt.le`	—	—
`arrow_mk_mapObj` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `mapObj` `CategoryTheory.SmallObject.SuccStruct.arrowMap`	—	`CategoryTheory.Arrow.arrow_mk_eqToHom_comp`
`congr_arrowMap` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.SmallObject.SuccStruct.arrowMap` `F`	—	`subsingleton` `LT.lt.le` `not_le`
`congr_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.map` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `LE.le.trans` `CategoryTheory.homOfLE` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.eqToHom` `congr_obj`	—	`CategoryTheory.Arrow.mk_eq_mk_iff` `congr_arrowMap` `LE.le.trans` `congr_obj`
`congr_obj` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F`	—	`subsingleton` `LE.le.trans` `le_of_lt`
`ext` 📖	—	`F`	—	—	`bot_le` `LT.lt.le`
`ext_iff` 📖	mathematical	—	`F`	—	`ext`
`mapObj_refl` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`mapObj` `LE.le.trans` `CategoryTheory.Functor.map` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `CategoryTheory.homOfLE`	—	`LE.le.trans` `CategoryTheory.Category.id_comp`
`mapObj_trans` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `mapObj` `LE.le.trans`	—	`LE.le.trans` `congr_obj` `congr_map` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp`
`mapObj_trans_assoc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `mapObj` `LE.le.trans`	—	`LE.le.trans` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mapObj_trans`
`obj_bot` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `bot_le` `CategoryTheory.SmallObject.SuccStruct.X₀`	—	—
`obj_limit` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `CategoryTheory.Limits.colimit` `Set.Iio` `CategoryTheory.SmallObject.restrictionLT` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit`	—	`LT.lt.le` `Order.IsSuccLimit.bot_lt` `arrowMap_limit`
`obj_succ` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `Order.succ` `Order.succ_le_of_lt` `CategoryTheory.SmallObject.SuccStruct.succ` `LT.lt.le`	—	`LT.lt.le` `arrowSucc_eq`
`prop_map_succ` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.SmallObject.SuccStruct.prop` `CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `F` `LT.lt.le` `Order.succ` `Order.succ_le_of_lt` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ`	—	`LT.lt.le` `Order.succ_le_of_lt` `Order.le_succ` `CategoryTheory.SmallObject.SuccStruct.prop_iff` `CategoryTheory.SmallObject.SuccStruct.arrowMap.eq_1` `CategoryTheory.SmallObject.SuccStruct.arrowSucc_def` `arrowSucc_eq`
`subsingleton` 📖	mathematical	—	`CategoryTheory.SmallObject.SuccStruct.Iteration`	—	`subsingleton.ext` `subsingleton.mapEq_refl` `obj_bot` `IsMin.eq_bot` `Order.le_succ` `CategoryTheory.Functor.congr_obj` `LE.le.trans` `CategoryTheory.SmallObject.SuccStruct.arrowMap_restrictionLE` `CategoryTheory.SmallObject.SuccStruct.arrowMap.congr_simp` `LE.le.lt_or_eq` `Order.lt_succ_iff_of_not_isMax` `subsingleton.mapEq_trans` `LT.lt.le` `Order.lt_succ_of_not_isMax` `Order.succ_le_of_lt` `CategoryTheory.SmallObject.SuccStruct.arrowSucc_def` `arrowSucc_eq` `subsingleton.MapEq.eq_1` `CategoryTheory.SmallObject.SuccStruct.arrowMap_refl` `obj_succ` `le_antisymm` `Order.succ_le_iff_of_not_isMax` `le_refl` `le_rfl` `CategoryTheory.Arrow.functor_ext` `arrowMap_limit` `CategoryTheory.SmallObject.SuccStruct.arrowι.congr_simp` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit` `obj_limit` `CategoryTheory.Limits.colimit.congr_simp` `ext`
`trunc_F` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`F` `trunc` `CategoryTheory.SmallObject.restrictionLE`	—	—

CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton

Definitions

Name	Category	Theorems
`MapEq` 📖	MathDef	1 math math: `mapEq_refl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`MapEq`	—	—	`CategoryTheory.Arrow.functor_ext`
`mapEq_refl` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership`	`MapEq`	—	`MapEq.eq_1` `CategoryTheory.SmallObject.SuccStruct.arrowMap_refl`
`mapEq_trans` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MapEq` `LE.le.trans`	—	—	`LE.le.trans` `MapEq.src` `MapEq.tgt` `CategoryTheory.homOfLE_comp` `CategoryTheory.Functor.map_comp` `MapEq.w` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.Category.id_comp`

CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`src` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `LE.le.trans`	—	—
`tgt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq`	`CategoryTheory.Functor.obj` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership`	—	—
`w` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq`	`CategoryTheory.Functor.map` `Set.Elem` `Set.Iic` `Preorder.smallCategory` `Subtype.preorder` `Set` `Set.instMembership` `LE.le.trans` `CategoryTheory.homOfLE` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.eqToHom`	—	`CategoryTheory.Arrow.mk_eq_mk_iff` `LE.le.trans`

CategoryTheory.SmallObject.SuccStruct.prop

Definitions

Name	Category	Theorems
`arrowIso` 📖	CompOp	4 math math: `arrowIso_hom_left`, `arrowIso_inv_left`, `arrowIso_inv_right`, `arrowIso_hom_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrowIso_hom_left` 📖	mathematical	`CategoryTheory.SmallObject.SuccStruct.prop`	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.id` `CategoryTheory.SmallObject.SuccStruct.toSuccArrow` `CategoryTheory.Iso.hom` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `arrowIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`arrowIso_hom_right` 📖	mathematical	`CategoryTheory.SmallObject.SuccStruct.prop`	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Functor.id` `CategoryTheory.SmallObject.SuccStruct.toSuccArrow` `CategoryTheory.Iso.hom` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `arrowIso` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SmallObject.SuccStruct.succ`	—	—
`arrowIso_inv_left` 📖	mathematical	`CategoryTheory.SmallObject.SuccStruct.prop`	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.id` `CategoryTheory.SmallObject.SuccStruct.toSuccArrow` `CategoryTheory.Iso.inv` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `arrowIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`arrowIso_inv_right` 📖	mathematical	`CategoryTheory.SmallObject.SuccStruct.prop`	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Functor.id` `CategoryTheory.SmallObject.SuccStruct.toSuccArrow` `CategoryTheory.Iso.inv` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `arrowIso` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SmallObject.SuccStruct.succ`	—	—
`fac` 📖	mathematical	`CategoryTheory.SmallObject.SuccStruct.prop`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SmallObject.SuccStruct.succ` `CategoryTheory.SmallObject.SuccStruct.toSucc` `CategoryTheory.eqToHom` `succ_eq`	—	`succ_eq` `CategoryTheory.Category.comp_id`
`fac_assoc` 📖	mathematical	`CategoryTheory.SmallObject.SuccStruct.prop`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SmallObject.SuccStruct.succ` `CategoryTheory.SmallObject.SuccStruct.toSucc` `CategoryTheory.eqToHom` `succ_eq`	—	`succ_eq` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`succ_eq` 📖	mathematical	`CategoryTheory.SmallObject.SuccStruct.prop`	`CategoryTheory.SmallObject.SuccStruct.succ`	—	—

---

← Back to Index