Documentation Verification Report

Rank

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

Statistics

Metric	Count
Definitions `rank`, `rank`	2
Theorems `le_succ_rank_sUnion`, `lt_rank_iff`, `rank_congr`, `rank_empty`, `rank_eq_wfRank`, `rank_insert`, `rank_le_iff`, `rank_lt_of_mem`, `rank_mono`, `rank_pair`, `rank_powerset`, `rank_sUnion_le`, `rank_singleton`, `le_succ_rank_sUnion`, `lt_rank_iff`, `rank_empty`, `rank_eq_wfRank`, `rank_iUnion`, `rank_insert`, `rank_le_iff`, `rank_lt_of_mem`, `rank_mk`, `rank_mono`, `rank_pair`, `rank_powerset`, `rank_range`, `rank_sUnion_le`, `rank_singleton`, `rank_union`	29
Total	31

PSet

Definitions

Name	Category	Theorems
`rank` 📖	CompOp	15 math math: `rank_le_iff`, `le_succ_rank_sUnion`, `rank_mono`, `rank_eq_wfRank`, `rank_lt_of_mem`, `ZFSet.rank_mk`, `rank_insert`, `rank_sUnion_le`, `Ordinal.rank_toPSet`, `rank_empty`, `rank_powerset`, `rank_singleton`, `lt_rank_iff`, `rank_congr`, `rank_pair`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_succ_rank_sUnion` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `Order.succ` `Ordinal.instSuccOrder` `sUnion`	—	`rank_powerset` `rank_mono` `subset_iff` `mem_powerset` `mem_sUnion`
`lt_rank_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `PSet` `instMembership` `Preorder.toLE`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_and_eq` `rank_le_iff`
`rank_congr` 📖	mathematical	`Equiv`	`rank`	—	`Set.ext`
`rank_empty` 📖	mathematical	—	`rank` `PSet` `instEmptyCollection` `Ordinal` `Ordinal.zero`	—	`empty_def` `ciSup_of_empty` `PEmpty.instIsEmpty` `bot_eq_zero'` `Ordinal.canonicallyOrderedAdd`
`rank_eq_wfRank` 📖	mathematical	—	`Ordinal.lift` `rank` `IsWellFounded.rank` `PSet` `instMembership` `instIsWellFoundedMem`	—	`mem_wf` `instIsWellFoundedMem` `IsWellFounded.rank_eq` `LE.le.antisymm` `le_of_forall_lt` `Ordinal.lt_lift_iff` `small_subtype` `UnivLE.small` `UnivLE.self` `Ordinal.instNoMaxOrder` `lt_rank_iff` `Ordinal.iSup_le` `rank_lt_of_mem`
`rank_insert` 📖	mathematical	—	`rank` `PSet` `instInsert` `Ordinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Order.succ` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`le_antisymm` `rank_congr` `Ordinal.instNoMaxOrder` `rank_lt_of_mem` `max_le` `LT.lt.succ_le` `mem_insert` `rank_mono` `subset_iff` `mem_insert_of_mem`
`rank_le_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `Preorder.toLT`	—	`LT.lt.trans_le` `rank_lt_of_mem` `Ordinal.iSup_le` `Order.succ_le_iff` `Ordinal.instNoMaxOrder`
`rank_lt_of_mem` 📖	mathematical	`PSet` `instMembership`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	`rank_congr` `Order.succ_le_iff` `Ordinal.instNoMaxOrder` `Ordinal.le_iSup` `UnivLE.small` `UnivLE.self`
`rank_mono` 📖	mathematical	`PSet` `instHasSubset`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	`rank_le_iff` `rank_lt_of_mem` `mem_of_subset`
`rank_pair` 📖	mathematical	—	`rank` `PSet` `instInsert` `instSingleton` `Ordinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Order.succ` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`rank_insert` `rank_singleton`
`rank_powerset` 📖	mathematical	—	`rank` `powerset` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`le_antisymm` `Ordinal.instNoMaxOrder` `rank_mono` `Order.succ_le_iff` `rank_lt_of_mem` `instReflSubset`
`rank_sUnion_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `sUnion`	—	`rank_lt_of_mem`
`rank_singleton` 📖	mathematical	—	`rank` `PSet` `instSingleton` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`rank_insert` `rank_empty` `sup_of_le_left` `Ordinal.canonicallyOrderedAdd`

ZFSet

Definitions

Name	Category	Theorems
`rank` 📖	CompOp	27 math math: `IsOrdinal.rank_le_iff_subset`, `subset_vonNeumann`, `rank_empty`, `lt_rank_iff`, `rank_mono`, `rank_mk`, `IsOrdinal.toZFSet_rank_eq`, `rank_powerset`, `subset_vonNeumann_self`, `rank_range`, `rank_insert`, `Ordinal.rank_toZFSet`, `mem_vonNeumann_succ`, `rank_le_iff`, `rank_iUnion`, `mem_vonNeumann`, `rank_eq_wfRank`, `rank_sUnion_le`, `rank_lt_of_mem`, `rank_pair`, `IsOrdinal.rank_lt_iff_mem`, `rank_singleton`, `rank_vonNeumann`, `Ordinal.toZFSetIso_symm_apply`, `rank_union`, `IsOrdinal.rank_inj`, `le_succ_rank_sUnion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_succ_rank_sUnion` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `Order.succ` `Ordinal.instSuccOrder` `sUnion`	—	`rank_powerset` `rank_mono` `mem_powerset` `mem_sUnion`
`lt_rank_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `ZFSet` `instMembership` `Preorder.toLE`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_and_eq` `rank_le_iff`
`rank_empty` 📖	mathematical	—	`rank` `ZFSet` `instEmptyCollection` `Ordinal` `Ordinal.zero`	—	`PSet.rank_empty`
`rank_eq_wfRank` 📖	mathematical	—	`Ordinal.lift` `rank` `IsWellFounded.rank` `ZFSet` `instMembership` `instIsWellFoundedMem`	—	`inductionOn` `instIsWellFoundedMem` `IsWellFounded.rank_eq` `LE.le.antisymm` `le_of_forall_lt` `Ordinal.lt_lift_iff` `small_subtype` `UnivLE.small` `UnivLE.self` `Ordinal.instNoMaxOrder` `lt_rank_iff` `Ordinal.iSup_le` `rank_lt_of_mem`
`rank_iUnion` 📖	mathematical	—	`rank` `iUnion` `iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot`	—	`le_antisymm` `LT.lt.trans_le` `rank_lt_of_mem` `Ordinal.le_iSup` `Ordinal.iSup_le` `rank_mono` `subset_iUnion`
`rank_insert` 📖	mathematical	—	`rank` `ZFSet` `instInsert` `Ordinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Order.succ` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`PSet.rank_insert`
`rank_le_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `Preorder.toLT`	—	`LT.lt.trans_le` `rank_lt_of_mem` `PSet.rank_le_iff`
`rank_lt_of_mem` 📖	mathematical	`ZFSet` `instMembership`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	`PSet.rank_lt_of_mem`
`rank_mk` 📖	mathematical	—	`rank` `PSet.rank`	—	—
`rank_mono` 📖	mathematical	`ZFSet` `instHasSubset`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	`rank_le_iff` `rank_lt_of_mem`
`rank_pair` 📖	mathematical	—	`rank` `ZFSet` `instInsert` `instSingleton` `Ordinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Order.succ` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`rank_insert` `rank_singleton`
`rank_powerset` 📖	mathematical	—	`rank` `powerset` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`PSet.rank_powerset`
`rank_range` 📖	mathematical	—	`rank` `range` `iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Order.succ` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`LE.le.antisymm'` `Ordinal.iSup_le` `Ordinal.instNoMaxOrder` `Ordinal.le_iSup`
`rank_sUnion_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank` `sUnion`	—	`rank_lt_of_mem`
`rank_singleton` 📖	mathematical	—	`rank` `ZFSet` `instSingleton` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder`	—	`rank_insert` `rank_empty` `sup_of_le_left` `Ordinal.canonicallyOrderedAdd`
`rank_union` 📖	mathematical	—	`rank` `ZFSet` `instUnion` `Ordinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot`	—	`le_antisymm` `rank_lt_of_mem` `max_le` `rank_mono`

---

← Back to Index