Commit 2024-12-15 00:44 161b962f

View on Github →

feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals (#17001) We previously defined ordinals as transitive sets, transitive under membership. This PR establishes this definition is equivalent to the following:

An ordinal is a transitive set of transitive sets
An ordinal is a transitive set of ordinals
An ordinal is a transitive set, trichotomous under membership
An ordinal is a transitive set, well-ordered under membership

Estimated changes

Modified Mathlib/Order/RelClasses.lean

added theorem WellFounded.asymmetric₃

added theorem WellFoundedRelation.asymmetric₃

Modified Mathlib/Order/RelIso/Set.lean

added theorem Subrel.coe_inclusionEmbedding

Modified Mathlib/SetTheory/ZFC/Ordinal.lean

added theorem ZFSet.IsOrdinal.mem_of_subset_of_mem

added theorem ZFSet.IsOrdinal.mem_or_subset

added theorem ZFSet.IsOrdinal.mem_trichotomous

added theorem ZFSet.IsOrdinal.not_mem_iff_subset

added theorem ZFSet.IsOrdinal.not_subset_iff_mem

added theorem ZFSet.IsOrdinal.subset_iff_eq_or_mem

added theorem ZFSet.IsOrdinal.subset_total

added theorem ZFSet.isOrdinal_empty

added theorem ZFSet.isOrdinal_iff_forall_mem_isOrdinal

added theorem ZFSet.isOrdinal_iff_forall_mem_isTransitive

modified theorem ZFSet.isOrdinal_iff_isTrans

added theorem ZFSet.isOrdinal_iff_isTrichotomous

added theorem ZFSet.isOrdinal_iff_isWellOrder

added theorem ZFSet.isOrdinal_not_mem_univ