Documentation Verification Report

SuccPredOrder

📁 Source: Mathlib/Data/Fin/SuccPredOrder.lean

Statistics

Metric	Count
Definitions `instPredOrder`, `instSuccOrder`	2
Theorems `orderPred_apply`, `orderPred_eq`, `orderPred_succ`, `orderPred_zero`, `orderSucc_apply`, `orderSucc_castSucc`, `orderSucc_eq`, `orderSucc_last`	8
Total	10

Fin

Definitions

Name	Category	Theorems
`instPredOrder` 📖	CompOp	4 math math: `orderPred_succ`, `orderPred_zero`, `orderPred_apply`, `orderPred_eq`
`instSuccOrder` 📖	CompOp	13 math math: `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app`, `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc`, `CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F`, `orderSucc_last`, `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F`, `orderSucc_apply`, `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv`, `CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot`, `CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app`, `orderSucc_castSucc`, `CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit`, `orderSucc_eq`, `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderPred_apply` 📖	mathematical	—	`Order.pred` `PartialOrder.toPreorder` `instPartialOrder` `instPredOrder`	—	—
`orderPred_eq` 📖	mathematical	—	`Order.pred` `PartialOrder.toPreorder` `instPartialOrder` `instPredOrder`	—	—
`orderPred_succ` 📖	mathematical	—	`Order.pred` `PartialOrder.toPreorder` `instPartialOrder` `instPredOrder`	—	—
`orderPred_zero` 📖	mathematical	—	`Order.pred` `PartialOrder.toPreorder` `instPartialOrder` `instPredOrder`	—	—
`orderSucc_apply` 📖	mathematical	—	`Order.succ` `PartialOrder.toPreorder` `instPartialOrder` `instSuccOrder`	—	—
`orderSucc_castSucc` 📖	mathematical	—	`Order.succ` `PartialOrder.toPreorder` `instPartialOrder` `instSuccOrder`	—	—
`orderSucc_eq` 📖	mathematical	—	`Order.succ` `PartialOrder.toPreorder` `instPartialOrder` `instSuccOrder`	—	—
`orderSucc_last` 📖	mathematical	—	`Order.succ` `PartialOrder.toPreorder` `instPartialOrder` `instSuccOrder`	—	—

---

← Back to Index