Documentation Verification Report

Rank

📁 Source: Mathlib/SetTheory/Ordinal/Rank.lean

Statistics

Metric	Count
Definitions `rank`, `rank`	2
Theorems `mem_range_rank_of_le`, `rank_eq`, `rank_lt_of_rel`, `mem_range_rank_of_le`, `rank_eq`, `rank_eq_typein`, `rank_lt_of_rel`, `rank_strictAnti`, `rank_strictMono`	9
Total	11

Acc

Definitions

Name	Category	Theorems
`rank` 📖	CompOp	2 math math: `rank_eq`, `rank_lt_of_rel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_range_rank_of_le` 📖	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	—	`LE.le.eq_or_lt` `Ordinal.lt_iSup_iff` `small_subtype` `UnivLE.small` `UnivLE.self` `rank_eq` `Order.lt_succ_iff` `Ordinal.instNoMaxOrder`
`rank_eq` 📖	mathematical	—	`rank` `iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Order.succ` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	—
`rank_lt_of_rel` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	`LT.lt.trans_le` `Order.lt_succ` `Ordinal.instNoMaxOrder` `rank_eq` `Ordinal.le_iSup` `small_subtype` `UnivLE.small` `univLE_of_max` `UnivLE.self`

IsWellFounded

Definitions

Name	Category	Theorems
`rank` 📖	CompOp	7 math math: `PSet.rank_eq_wfRank`, `WellFoundedGT.rank_strictAnti`, `rank_lt_of_rel`, `rank_eq_typein`, `rank_eq`, `WellFoundedLT.rank_strictMono`, `ZFSet.rank_eq_wfRank`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_range_rank_of_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	`Set` `Set.instMembership` `Set.range`	—	`Acc.mem_range_rank_of_le` `apply`
`rank_eq` 📖	mathematical	—	`rank` `iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Order.succ` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`Acc.rank_eq` `apply`
`rank_eq_typein` 📖	mathematical	—	`rank` `IsWellOrder.toIsWellFounded` `DFunLike.coe` `RelEmbedding` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `Ordinal.typein`	—	`IsWellOrder.toIsWellFounded` `InitialSeg.eq` `instIsStrictTotalOrderOfIsWellOrder` `isWellOrder_lt` `Ordinal.wellFoundedLT` `WellFoundedLT.rank_strictMono` `mem_range_rank_of_le` `LT.lt.le` `PrincipalSeg.mem_range_of_rel` `instIsTransLt`
`rank_lt_of_rel` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	`Acc.rank_lt_of_rel` `apply`

WellFoundedGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_strictAnti` 📖	mathematical	—	`StrictAnti` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `IsWellFounded.rank` `Preorder.toLT`	—	`IsWellFounded.rank_lt_of_rel`

WellFoundedLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `IsWellFounded.rank` `Preorder.toLT`	—	`IsWellFounded.rank_lt_of_rel`

---

← Back to Index