RankNat

Statistics

Metric	Count
Definitions `rank`, `rank'`, `rankFunction`	3
Theorems `instFiniteSubtypeElemNIIAncestralRel`, `instNonemptyRankFunctionNat`, `instNonemptyWeakRankFunctionNat`, `isRegular_iff_nonempty_rankFunction`, `isRegular_iff_nonempty_weakRankFunction`, `rank'_eq`, `rank'_lt`, `rank_lt`	8
Total	11

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteSubtypeElemNIIAncestralRel` 📖	mathematical	—	`Finite` `Set.Elem` `SSet.Subcomplex.N` `II` `AncestralRel`	—	`SSet.N.le_iff_exists_mono` `LT.lt.le` `SSet.N.dim_lt_of_lt` `SSet.S.ext_iff` `Finite.of_injective` `Finite.instSigma` `Finite.of_fintype` `SimplexCategory.instFiniteHom` `SSet.Subcomplex.N.ext_iff` `SSet.N.ext_iff`
`instNonemptyRankFunctionNat` 📖	mathematical	—	`RankFunction` `Nat.instPartialOrder`	—	—
`instNonemptyWeakRankFunctionNat` 📖	mathematical	—	`WeakRankFunction` `Nat.instPartialOrder`	—	—
`isRegular_iff_nonempty_rankFunction` 📖	mathematical	—	`IsRegular` `RankFunction` `Nat.instPartialOrder`	—	`instNonemptyRankFunctionNat` `RankFunction.isRegular` `instWellFoundedLTNat`
`isRegular_iff_nonempty_weakRankFunction` 📖	mathematical	—	`IsRegular` `WeakRankFunction` `Nat.instPartialOrder`	—	`instNonemptyWeakRankFunctionNat` `WeakRankFunction.isRegular` `instWellFoundedLTNat`
`rank'_eq` 📖	mathematical	`Set.Elem` `SSet.Subcomplex.N` `II` `AncestralRel`	`rank'` `iSup` `Nat.instSupSet`	—	—
`rank'_lt` 📖	mathematical	`Set.Elem` `SSet.Subcomplex.N` `II` `AncestralRel`	`rank'`	—	`rank'_eq` `le_csSup` `Finite.bddAbove_range` `instFiniteSubtypeElemNIIAncestralRel` `SemilatticeSup.instIsDirectedOrder`
`rank_lt` 📖	mathematical	`AncestralRel`	`rank`	—	`rank'_lt`

---