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	22 math math: enumOrd_range, enumOrd_le_enumOrd, enumOrd_inj, enumOrd_zero, enumOrd_mem, isNormal_enumOrd, coe_preOmega, deriv_eq_enumOrd, enumOrd_le_of_forall_lt, enumOrd_le_of_subset, enumOrd_succ_le, 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	Ordinal enumOrd	—	StrictMono.injective enumOrd_strictMono
enumOrd_le_enumOrd 📖	mathematical	BddAbove Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	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	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder enumOrd	—	csInf_le'
enumOrd_le_of_subset 📖	mathematical	BddAbove Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder Set Set.instHasSubset	Pi.hasLe Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder 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	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder enumOrd	—	StrictMono.lt_iff_lt enumOrd_strictMono
enumOrd_mem 📖	mathematical	BddAbove Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	Ordinal Set Set.instMembership enumOrd	—	—
enumOrd_range 📖	mathematical	StrictMono Ordinal PartialOrder.toPreorder partialOrder	enumOrd Set.range Ordinal	—	eq_enumOrd StrictMono.not_bddAbove_range_of_wellFoundedLT wellFoundedLT instNoMaxOrder
enumOrd_strictMono 📖	mathematical	BddAbove Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	StrictMono Ordinal PartialOrder.toPreorder partialOrder enumOrd	—	—
enumOrd_succ_le 📖	mathematical	BddAbove Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder Set Set.instMembership Preorder.toLT enumOrd	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder 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	Ordinal 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 Ordinal PartialOrder.toPreorder partialOrder Set.range	—	enumOrd_strictMono range_enumOrd wellFoundedLT
id_le_enumOrd 📖	mathematical	BddAbove Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	Pi.hasLe Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder 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 Ordinal 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	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 Ordinal 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