Documentation Verification Report

Preorder

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

Statistics

Metric	Count
Definitions `orderBot`, `orderTop`, `coconeOfUpperBound`, `colimitCoconeOfIsLUB`, `coneOfLowerBound`, `isColimitBinaryCofan`, `isColimitOfIsLUB`, `isInitialBot`, `isLimitBinaryFan`, `isLimitOfIsGLB`, `isTerminalTop`, `limitConeOfIsGLB`, `orderBotOfHasInitial`, `orderTopOfHasTerminal`, `semilatticeInfOfHasBinaryProducts`, `semilatticeInfOfIsLimitBinaryFan`, `semilatticeSupOfHasBinaryCoproducts`, `semilatticeSupOfIsColimitBinaryCofan`	18
Theorems `coconeOfUpperBound_pt`, `coconeOfUpperBound_ι_app`, `coconePt_mem_upperBounds`, `colimitCoconeOfIsLUB_cocone`, `colimitCoconeOfIsLUB_isColimit`, `coneOfLowerBound_pt`, `coneOfLowerBound_π_app`, `conePt_mem_lowerBounds`, `hasColimit_iff_hasLUB`, `hasLimit_iff_hasGLB`, `instHasBinaryCoproducts`, `instHasBinaryProducts`, `instHasInitialOfOrderBot`, `instHasTerminalOfOrderTop`, `isGLB_of_isLimit`, `isLUB_of_isColimit`, `limitConeOfIsGLB_cone`, `limitConeOfIsGLB_isLimit`	18
Total	36

CategoryTheory.Limits.IsInitial

Definitions

Name	Category	Theorems
`orderBot` 📖	CompOp	—

CategoryTheory.Limits.IsTerminal

Definitions

Name	Category	Theorems
`orderTop` 📖	CompOp	—

Preorder

Definitions

Name	Category	Theorems
`coconeOfUpperBound` 📖	CompOp	4 math math: `colimitCoconeOfIsLUB_cocone`, `colimitCoconeOfIsLUB_isColimit`, `coconeOfUpperBound_pt`, `coconeOfUpperBound_ι_app`
`colimitCoconeOfIsLUB` 📖	CompOp	2 math math: `colimitCoconeOfIsLUB_cocone`, `colimitCoconeOfIsLUB_isColimit`
`coneOfLowerBound` 📖	CompOp	4 math math: `limitConeOfIsGLB_isLimit`, `limitConeOfIsGLB_cone`, `coneOfLowerBound_pt`, `coneOfLowerBound_π_app`
`isColimitBinaryCofan` 📖	CompOp	—
`isColimitOfIsLUB` 📖	CompOp	1 math math: `colimitCoconeOfIsLUB_isColimit`
`isInitialBot` 📖	CompOp	—
`isLimitBinaryFan` 📖	CompOp	—
`isLimitOfIsGLB` 📖	CompOp	1 math math: `limitConeOfIsGLB_isLimit`
`isTerminalTop` 📖	CompOp	—
`limitConeOfIsGLB` 📖	CompOp	2 math math: `limitConeOfIsGLB_isLimit`, `limitConeOfIsGLB_cone`
`orderBotOfHasInitial` 📖	CompOp	—
`orderTopOfHasTerminal` 📖	CompOp	—
`semilatticeInfOfHasBinaryProducts` 📖	CompOp	—
`semilatticeInfOfIsLimitBinaryFan` 📖	CompOp	—
`semilatticeSupOfHasBinaryCoproducts` 📖	CompOp	—
`semilatticeSupOfIsColimitBinaryCofan` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coconeOfUpperBound_pt` 📖	mathematical	`Set` `Set.instMembership` `upperBounds` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.Limits.Cocone.pt` `coconeOfUpperBound`	—	—
`coconeOfUpperBound_ι_app` 📖	mathematical	`Set` `Set.instMembership` `upperBounds` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι` `coconeOfUpperBound` `CategoryTheory.homOfLE`	—	—
`coconePt_mem_upperBounds` 📖	mathematical	—	`Set` `Set.instMembership` `upperBounds` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory` `CategoryTheory.Limits.Cocone.pt`	—	—
`colimitCoconeOfIsLUB_cocone` 📖	mathematical	`IsLUB` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.Limits.ColimitCocone.cocone` `colimitCoconeOfIsLUB` `coconeOfUpperBound`	—	—
`colimitCoconeOfIsLUB_isColimit` 📖	mathematical	`IsLUB` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.Limits.ColimitCocone.isColimit` `colimitCoconeOfIsLUB` `isColimitOfIsLUB` `coconeOfUpperBound`	—	—
`coneOfLowerBound_pt` 📖	mathematical	`Set` `Set.instMembership` `lowerBounds` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.Limits.Cone.pt` `coneOfLowerBound`	—	—
`coneOfLowerBound_π_app` 📖	mathematical	`Set` `Set.instMembership` `lowerBounds` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.π` `coneOfLowerBound` `CategoryTheory.homOfLE`	—	—
`conePt_mem_lowerBounds` 📖	mathematical	—	`Set` `Set.instMembership` `lowerBounds` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory` `CategoryTheory.Limits.Cone.pt`	—	—
`hasColimit_iff_hasLUB` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `smallCategory` `IsLUB` `toLE` `Set.range` `CategoryTheory.Functor.obj`	—	`isLUB_of_isColimit`
`hasLimit_iff_hasGLB` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `smallCategory` `IsGLB` `toLE` `Set.range` `CategoryTheory.Functor.obj`	—	`isGLB_of_isLimit`
`instHasBinaryCoproducts` 📖	mathematical	—	`CategoryTheory.Limits.HasBinaryCoproducts` `smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`le_sup_left` `le_sup_right` `CategoryTheory.Limits.hasColimit_of_iso`
`instHasBinaryProducts` 📖	mathematical	—	`CategoryTheory.Limits.HasBinaryProducts` `smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`inf_le_left` `inf_le_right` `CategoryTheory.Limits.hasLimit_of_iso`
`instHasInitialOfOrderBot` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial` `smallCategory`	—	`CategoryTheory.Limits.hasInitial_of_unique` `subsingleton_hom`
`instHasTerminalOfOrderTop` 📖	mathematical	—	`CategoryTheory.Limits.HasTerminal` `smallCategory`	—	`CategoryTheory.Limits.hasTerminal_of_unique` `subsingleton_hom`
`isGLB_of_isLimit` 📖	mathematical	—	`IsGLB` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory` `CategoryTheory.Limits.Cone.pt`	—	`conePt_mem_lowerBounds`
`isLUB_of_isColimit` 📖	mathematical	—	`IsLUB` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory` `CategoryTheory.Limits.Cocone.pt`	—	`coconePt_mem_upperBounds`
`limitConeOfIsGLB_cone` 📖	mathematical	`IsGLB` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.Limits.LimitCone.cone` `limitConeOfIsGLB` `coneOfLowerBound`	—	—
`limitConeOfIsGLB_isLimit` 📖	mathematical	`IsGLB` `toLE` `Set.range` `CategoryTheory.Functor.obj` `smallCategory`	`CategoryTheory.Limits.LimitCone.isLimit` `limitConeOfIsGLB` `isLimitOfIsGLB` `coneOfLowerBound`	—	—

---

← Back to Index