Documentation Verification Report

Enum

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

Statistics

Metric	Count
Definitions `enumOrd`, `enumOrdOrderIso`	2
Theorems `enumOrd_inj`, `enumOrd_injective`, `enumOrd_le_enumOrd`, `enumOrd_le_of_forall_lt`, `enumOrd_le_of_subset`, `enumOrd_lt_enumOrd`, `enumOrd_mem`, `enumOrd_range`, `enumOrd_strictMono`, `enumOrd_succ_le`, `enumOrd_surjective`, `enumOrd_univ`, `enumOrd_zero`, `eq_enumOrd`, `id_le_enumOrd`, `isNormal_enumOrd`, `le_enumOrd_self`, `range_enumOrd`	18
Total	20

Ordinal

Definitions

Name	Category	Theorems
`enumOrd` 📖	CompOp	20 math math: `enumOrd_range`, `enumOrd_le_enumOrd`, `enumOrd_inj`, `enumOrd_zero`, `enumOrd_mem`, `isNormal_enumOrd`, `coe_preOmega`, `deriv_eq_enumOrd`, `enumOrd_le_of_subset`, `le_enumOrd_self`, `enumOrd_surjective`, `enumOrd_lt_enumOrd`, `enumOrd_isNormal_iff_isClosed`, `enumOrd_univ`, `id_le_enumOrd`, `enumOrd_injective`, `range_enumOrd`, `enumOrd_strictMono`, `eq_enumOrd`, `derivFamily_eq_enumOrd`
`enumOrdOrderIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`enumOrd_inj` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`enumOrd`	—	`enumOrd_injective`
`enumOrd_injective` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`enumOrd`	—	`StrictMono.injective` `enumOrd_strictMono`
`enumOrd_le_enumOrd` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`enumOrd`	—	`StrictMono.le_iff_le` `enumOrd_strictMono`
`enumOrd_le_of_forall_lt` 📖	mathematical	`Ordinal` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `enumOrd`	`Preorder.toLE`	—	`csInf_le'`
`enumOrd_le_of_subset` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Set` `Set.instHasSubset`	`Pi.hasLe` `enumOrd`	—	`csInf_le_csInf'` `Set.inter_subset_inter` `Set.setOf_subset_setOf_of_imp` `Mathlib.Tactic.GCongr.imp_right_mono` `lt_imp_lt_of_le_of_le` `le_refl`
`enumOrd_lt_enumOrd` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Preorder.toLT` `enumOrd`	—	`StrictMono.lt_iff_lt` `enumOrd_strictMono`
`enumOrd_mem` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Set` `Set.instMembership` `enumOrd`	—	—
`enumOrd_range` 📖	mathematical	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`enumOrd` `Set.range`	—	`eq_enumOrd` `StrictMono.not_bddAbove_range_of_wellFoundedLT` `wellFoundedLT` `instNoMaxOrder`
`enumOrd_strictMono` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`StrictMono` `enumOrd`	—	—
`enumOrd_succ_le` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Set` `Set.instMembership` `Preorder.toLT` `enumOrd`	`Order.succ` `instSuccOrder`	—	`enumOrd_le_of_forall_lt` `LE.le.trans_lt` `StrictMono.monotone` `enumOrd_strictMono` `Order.lt_succ_iff` `instNoMaxOrder`
`enumOrd_surjective` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Set` `Set.instMembership`	`enumOrd`	—	`range_enumOrd`
`enumOrd_univ` 📖	mathematical	—	`enumOrd` `Set.univ` `Ordinal`	—	`Set.range_id` `enumOrd_range` `strictMono_id`
`enumOrd_zero` 📖	mathematical	—	`enumOrd` `Ordinal` `zero` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`canonicallyOrderedAdd` `instIsEmptyFalse` `Set.inter_univ`
`eq_enumOrd` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`enumOrd` `StrictMono` `Set.range`	—	`enumOrd_strictMono` `range_enumOrd` `wellFoundedLT`
`id_le_enumOrd` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Pi.hasLe` `enumOrd`	—	`StrictMono.id_le` `wellFoundedLT` `enumOrd_strictMono`
`isNormal_enumOrd` 📖	mathematical	`Ordinal` `Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Order.IsNormal` `instLinearOrder` `enumOrd`	—	`Order.isNormal_iff` `enumOrd_strictMono` `enumOrd_le_of_forall_lt` `Order.IsSuccLimit.bot_lt` `enumOrd_mem` `Set.range_nonempty` `bddAbove_of_small` `small_range` `small_Iio` `LT.lt.trans_le` `Order.lt_succ` `instNoMaxOrder` `le_iSup` `Order.IsSuccLimit.succ_lt` `iSup_le`
`le_enumOrd_self` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`enumOrd`	—	`StrictMono.le_apply` `wellFoundedLT` `enumOrd_strictMono`
`range_enumOrd` 📖	mathematical	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Set.range` `enumOrd`	—	`Set.ext` `enumOrd_mem` `LE.le.antisymm` `enumOrd_le_of_forall_lt` `LT.lt.not_ge` `csInf_le'` `csInf_mem` `wellFoundedLT` `StrictMono.id_le` `enumOrd_strictMono`

---

← Back to Index