Commit 2023-04-10 15:18 b9e5e441

View on Github →

feat: port SetTheory.ZFC.Ordinal (#3334) Also corrects the folder casing Zfc to ZFC.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/SetTheory/Zfc/Basic.lean to Mathlib/SetTheory/ZFC/Basic.lean

Created Mathlib/SetTheory/ZFC/Ordinal.lean

added theorem ZFSet.IsTransitive.subset_of_mem

added theorem ZFSet.IsTransitive.unionₛ'

added def ZFSet.IsTransitive

added theorem ZFSet.empty_isTransitive

added theorem ZFSet.isTransitive_iff_mem_trans

added theorem ZFSet.isTransitive_iff_subset_powerset

added theorem ZFSet.isTransitive_iff_unionₛ_subset