Ordinal

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

Statistics

Metric	Count
Definitions toPSet, toZFSet, toZFSetIso, IsOrdinal, IsTransitive	5
Theorems card_toZFSet, coe_toZFSet, mem_toPSet_iff, mem_toZFSet_iff, mk_toPSet, rank_toPSet, rank_toZFSet, toZFSetIso_apply, toZFSetIso_symm_apply, toZFSet_injective, toZFSet_mem_toZFSet_iff, toZFSet_monotone, toZFSet_strictMono, toZFSet_subset_toZFSet_iff, toZFSet_succ, toZFSet_zero, type_toPSet, eq_or_mem_of_subset, isTrans, isTransitive, isTrichotomous, isWellOrder, mem, mem_of_subset_of_mem, mem_or_subset, mem_trans, mem_trans', mem_trichotomous, notMem_iff_subset, not_subset_iff_mem, rank_inj, rank_le_iff_subset, rank_lt_iff_mem, subset_iff_eq_or_mem, subset_of_mem, subset_total, toZFSet_rank_eq, trichotomous, iUnion, inter, mem_trans, powerset, sUnion, sUnion', sUnion_subset, subset_of_mem, subset_powerset, union, isOrdinal_empty, isOrdinal_iff_forall_mem_isOrdinal, isOrdinal_iff_forall_mem_isTransitive, isOrdinal_iff_isTrans, isOrdinal_iff_isTrichotomous, isOrdinal_iff_isWellOrder, isOrdinal_iff_mem_range_toZFSet, isOrdinal_iff_trichotomous, isOrdinal_succ, isOrdinal_toZFSet, isTransitive_empty, isTransitive_iff_mem_trans, isTransitive_iff_sUnion_subset, isTransitive_iff_subset_powerset	62
Total	67

Ordinal

Definitions

Name	Category	Theorems
toPSet 📖	CompOp	4 math math: mk_toPSet, mem_toPSet_iff, rank_toPSet, type_toPSet
toZFSet 📖	CompOp	17 math math: coe_toZFSet, mem_toZFSet_iff, ZFSet.isOrdinal_iff_mem_range_toZFSet, ZFSet.IsOrdinal.toZFSet_rank_eq, toZFSet_strictMono, mk_toPSet, card_toZFSet, ZFSet.isOrdinal_toZFSet, toZFSetIso_apply, toZFSet_subset_vonNeumann, rank_toZFSet, toZFSet_injective, toZFSet_subset_toZFSet_iff, toZFSet_monotone, toZFSet_zero, toZFSet_succ, toZFSet_mem_toZFSet_iff
toZFSetIso 📖	CompOp	2 math math: toZFSetIso_apply, toZFSetIso_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_toZFSet 📖	mathematical	—	ZFSet.card toZFSet card	—	ZFSet.cardinalMk_coe_sort mk_Iio_ordinal Cardinal.mk_image_eq toZFSet_injective
coe_toZFSet 📖	mathematical	—	SetLike.coe ZFSet ZFSet.instSetLike toZFSet Set.image Ordinal Set.Iio PartialOrder.toPreorder partialOrder	—	Set.ext
mem_toPSet_iff 📖	mathematical	—	PSet PSet.instMembership toPSet Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder PSet.Equiv	—	toPSet.eq_1 PSet.mem_def Equiv.exists_congr_left
mem_toZFSet_iff 📖	mathematical	—	ZFSet ZFSet.instMembership toZFSet Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder	—	toZFSet.eq_1 ZFSet.mk_eq ZFSet.mk_mem_iff mem_toPSet_iff ZFSet.eq PSet.Equiv.comm
mk_toPSet 📖	mathematical	—	toPSet toZFSet	—	—
rank_toPSet 📖	mathematical	—	PSet.rank toPSet	—	toPSet.eq_1 PSet.rank.eq_1 iSup_succ Equiv.iSup_comp
rank_toZFSet 📖	mathematical	—	ZFSet.rank toZFSet	—	rank_toPSet
toZFSetIso_apply 📖	mathematical	—	DFunLike.coe RelIso Ordinal ZFSet ZFSet.IsOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder ZFSet.instPartialOrder RelIso.instFunLike toZFSetIso toZFSet ZFSet.isOrdinal_toZFSet	—	—
toZFSetIso_symm_apply 📖	mathematical	—	DFunLike.coe RelIso ZFSet ZFSet.IsOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder ZFSet.instPartialOrder partialOrder RelIso.instFunLike RelIso.symm toZFSetIso ZFSet.rank	—	—
toZFSet_injective 📖	mathematical	—	Ordinal ZFSet toZFSet	—	StrictMono.injective toZFSet_strictMono
toZFSet_mem_toZFSet_iff 📖	mathematical	—	ZFSet ZFSet.instMembership toZFSet Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder	—	Mathlib.Tactic.Contrapose.contrapose₁ ZFSet.notMem_of_subset toZFSet_monotone
toZFSet_monotone 📖	mathematical	—	Monotone Ordinal ZFSet PartialOrder.toPreorder partialOrder ZFSet.instPartialOrder toZFSet	—	mem_toZFSet_iff LT.lt.trans_le
toZFSet_strictMono 📖	mathematical	—	StrictMono Ordinal ZFSet PartialOrder.toPreorder partialOrder ZFSet.instPartialOrder toZFSet	—	ZFSet.instIsNonstrictStrictOrderSubsetSSubset LT.lt.le
toZFSet_subset_toZFSet_iff 📖	mathematical	—	ZFSet ZFSet.instHasSubset toZFSet Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	—	Mathlib.Tactic.Contrapose.contrapose₁ ZFSet.not_subset_of_mem toZFSet_monotone
toZFSet_succ 📖	mathematical	—	toZFSet Order.succ Ordinal PartialOrder.toPreorder partialOrder instSuccOrder ZFSet ZFSet.instInsert	—	ZFSet.ext instNoMaxOrder
toZFSet_zero 📖	mathematical	—	toZFSet Ordinal zero ZFSet ZFSet.instEmptyCollection	—	ZFSet.ext canonicallyOrderedAdd
type_toPSet 📖	mathematical	—	PSet.Type toPSet ToType	—	toPSet.eq_1

ZFSet

Definitions

Name	Category	Theorems
IsOrdinal 📖	CompData	12 math math: isOrdinal_iff_forall_mem_isTransitive, isOrdinal_empty, isOrdinal_notMem_univ, isOrdinal_iff_mem_range_toZFSet, isOrdinal_toZFSet, Ordinal.toZFSetIso_apply, isOrdinal_iff_isTrans, isOrdinal_iff_isTrichotomous, isOrdinal_iff_trichotomous, isOrdinal_iff_isWellOrder, isOrdinal_iff_forall_mem_isOrdinal, Ordinal.toZFSetIso_symm_apply
IsTransitive 📖	MathDef	12 math math: isOrdinal_iff_forall_mem_isTransitive, IsOrdinal.isTransitive, isOrdinal_iff_isTrans, isTransitive_iff_subset_powerset, isTransitive_empty, isOrdinal_iff_isTrichotomous, isOrdinal_iff_trichotomous, isOrdinal_iff_isWellOrder, isTransitive_iff_mem_trans, isOrdinal_iff_forall_mem_isOrdinal, isTransitive_vonNeumann, isTransitive_iff_sUnion_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrdinal_empty 📖	mathematical	—	IsOrdinal ZFSet instEmptyCollection	—	isTransitive_empty notMem_empty
isOrdinal_iff_forall_mem_isOrdinal 📖	mathematical	—	IsOrdinal IsTransitive	—	IsOrdinal.isTransitive IsOrdinal.mem isOrdinal_iff_forall_mem_isTransitive
isOrdinal_iff_forall_mem_isTransitive 📖	mathematical	—	IsOrdinal IsTransitive	—	IsOrdinal.isTransitive IsOrdinal.mem IsTransitive.mem_trans
isOrdinal_iff_isTrans 📖	mathematical	—	IsOrdinal IsTransitive IsTrans ZFSet instMembership Subrel	—	IsOrdinal.isTransitive IsOrdinal.isTrans IsTransitive.mem_trans
isOrdinal_iff_isTrichotomous 📖	mathematical	—	IsOrdinal IsTransitive ZFSet instMembership Subrel	—	isOrdinal_iff_trichotomous
isOrdinal_iff_isWellOrder 📖	mathematical	—	IsOrdinal IsTransitive IsWellOrder ZFSet instMembership Subrel	—	IsOrdinal.isTransitive IsOrdinal.isWellOrder isOrdinal_iff_isTrans IsWellOrder.toIsTrans
isOrdinal_iff_mem_range_toZFSet 📖	mathematical	—	IsOrdinal ZFSet Set Set.instMembership Set.range Ordinal Ordinal.toZFSet	—	IsOrdinal.toZFSet_rank_eq Set.mem_range_self isOrdinal_toZFSet
isOrdinal_iff_trichotomous 📖	mathematical	—	IsOrdinal IsTransitive ZFSet instMembership Subrel	—	IsOrdinal.isTransitive IsOrdinal.trichotomous isOrdinal_iff_isTrans trichotomous_of asymm Subrel.instAsymmSubtype instAsymmOfIsWellFounded instIsWellFoundedMem WellFounded.asymmetric₃ mem_wf
isOrdinal_succ 📖	mathematical	IsOrdinal	ZFSet instInsert	—	mem_insert_iff HasSubset.Subset.trans instIsTransSubset IsOrdinal.subset_of_mem IsOrdinal.mem_trans IsOrdinal.mem_trans'
isOrdinal_toZFSet 📖	mathematical	—	IsOrdinal Ordinal.toZFSet	—	Ordinal.mem_toZFSet_iff Ordinal.toZFSet_mem_toZFSet_iff LT.lt.trans
isTransitive_empty 📖	mathematical	—	IsTransitive ZFSet instEmptyCollection	—	notMem_empty
isTransitive_iff_mem_trans 📖	mathematical	—	IsTransitive ZFSet instMembership	—	IsTransitive.subset_of_mem
isTransitive_iff_sUnion_subset 📖	mathematical	—	IsTransitive ZFSet instHasSubset sUnion	—	mem_sUnion IsTransitive.mem_trans mem_sUnion_of_mem
isTransitive_iff_subset_powerset 📖	mathematical	—	IsTransitive ZFSet instHasSubset powerset	—	mem_powerset IsTransitive.subset_of_mem

ZFSet.IsOrdinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_or_mem_of_subset 📖	mathematical	ZFSet.IsOrdinal ZFSet ZFSet.instHasSubset	ZFSet.instMembership	—	subset_iff_eq_or_mem
isTrans 📖	mathematical	ZFSet.IsOrdinal	IsTrans ZFSet ZFSet.instMembership Subrel	—	mem_trans'
isTransitive 📖	mathematical	ZFSet.IsOrdinal	ZFSet.IsTransitive	—	—
isTrichotomous 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instMembership Subrel	—	trichotomous
isWellOrder 📖	mathematical	ZFSet.IsOrdinal	IsWellOrder ZFSet ZFSet.instMembership Subrel	—	trichotomous isTrans RelEmbedding.wellFounded ZFSet.mem_wf
mem 📖	—	ZFSet.IsOrdinal ZFSet ZFSet.instMembership	—	—	isTrans subset_of_mem ZFSet.isOrdinal_iff_isTrans mem_trans' RelEmbedding.isTrans
mem_of_subset_of_mem 📖	—	ZFSet.IsOrdinal ZFSet ZFSet.instHasSubset ZFSet.instMembership	—	—	eq_or_mem_of_subset mem mem_trans
mem_or_subset 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instMembership ZFSet.instHasSubset	—	notMem_iff_subset
mem_trans 📖	—	ZFSet.IsOrdinal ZFSet ZFSet.instMembership	—	—	ZFSet.IsTransitive.mem_trans isTransitive
mem_trans' 📖	—	ZFSet.IsOrdinal ZFSet ZFSet.instMembership	—	—	—
mem_trichotomous 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instMembership	—	subset_iff_eq_or_mem mem_or_subset
notMem_iff_subset 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instMembership ZFSet.instHasSubset	—	Sym2.GameAdd.induction ZFSet.mem_wf mem_of_subset_of_mem Sym2.GameAdd.fst_snd mem ZFSet.mem_irrefl
not_subset_iff_mem 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instHasSubset ZFSet.instMembership	—	not_iff_comm notMem_iff_subset
rank_inj 📖	mathematical	ZFSet.IsOrdinal	ZFSet.rank	—	le_antisymm_iff subset_antisymm_iff ZFSet.instReflSubset ZFSet.instAntisymmSubset rank_le_iff_subset
rank_le_iff_subset 📖	mathematical	ZFSet.IsOrdinal	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder ZFSet.rank ZFSet ZFSet.instHasSubset	—	notMem_iff_subset rank_lt_iff_mem not_lt
rank_lt_iff_mem 📖	mathematical	ZFSet.IsOrdinal	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ZFSet.rank ZFSet ZFSet.instMembership	—	not_subset_iff_mem LE.le.not_gt ZFSet.rank_mono ZFSet.rank_lt_of_mem
subset_iff_eq_or_mem 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instHasSubset ZFSet.instMembership	—	Sym2.GameAdd.induction ZFSet.mem_wf subset_antisymm ZFSet.instAntisymmSubset WellFounded.has_min Set.diff_nonempty mem_trans Sym2.GameAdd.fst_snd mem Set.notMem_of_mem_diff subset_refl ZFSet.instReflSubset subset_of_mem
subset_of_mem 📖	mathematical	ZFSet.IsOrdinal ZFSet ZFSet.instMembership	ZFSet.instHasSubset	—	ZFSet.IsTransitive.subset_of_mem isTransitive
subset_total 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instHasSubset	—	mem_or_subset subset_of_mem
toZFSet_rank_eq 📖	mathematical	ZFSet.IsOrdinal	Ordinal.toZFSet ZFSet.rank	—	ZFSet.isOrdinal_toZFSet Ordinal.rank_toZFSet
trichotomous 📖	mathematical	ZFSet.IsOrdinal	ZFSet ZFSet.instMembership Subrel	—	mem_trichotomous mem

ZFSet.IsTransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iUnion 📖	mathematical	ZFSet.IsTransitive	ZFSet.iUnion	—	sUnion'
inter 📖	mathematical	ZFSet.IsTransitive	ZFSet ZFSet.instInter	—	ZFSet.mem_inter mem_trans
mem_trans 📖	—	ZFSet.IsTransitive ZFSet ZFSet.instMembership	—	—	ZFSet.isTransitive_iff_mem_trans
powerset 📖	mathematical	ZFSet.IsTransitive	ZFSet.powerset	—	ZFSet.mem_powerset subset_of_mem
sUnion 📖	mathematical	ZFSet.IsTransitive	ZFSet.sUnion	—	ZFSet.mem_sUnion ZFSet.mem_sUnion_of_mem mem_trans
sUnion' 📖	mathematical	ZFSet.IsTransitive	ZFSet.sUnion	—	ZFSet.mem_sUnion ZFSet.mem_sUnion_of_mem mem_trans
sUnion_subset 📖	mathematical	ZFSet.IsTransitive	ZFSet ZFSet.instHasSubset ZFSet.sUnion	—	ZFSet.isTransitive_iff_sUnion_subset
subset_of_mem 📖	mathematical	ZFSet.IsTransitive ZFSet ZFSet.instMembership	ZFSet.instHasSubset	—	—
subset_powerset 📖	mathematical	ZFSet.IsTransitive	ZFSet ZFSet.instHasSubset ZFSet.powerset	—	ZFSet.isTransitive_iff_subset_powerset
union 📖	mathematical	ZFSet.IsTransitive	ZFSet ZFSet.instUnion	—	ZFSet.sUnion_pair sUnion' ZFSet.mem_pair

---

← Back to Index