Commit 2024-10-25 20:32 1a5abab1

View on Github →

feat(SetTheory/Ordinal/Topology): define Ordinal.IsClosed and Ordinal.IsAcc (#16710) Defined Ordinal.IsClosed and Ordinal.IsAcc and proved basic lemmas about them. This is closedness in the club-sense.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.isLimit_of_not_succ_of_ne_zero

Modified Mathlib/SetTheory/Ordinal/Topology.lean

added theorem Ordinal.IsAcc.forall_lt

added theorem Ordinal.IsAcc.inter_Ioo_nonempty

added theorem Ordinal.IsAcc.isLimit

added theorem Ordinal.IsAcc.mono

added theorem Ordinal.IsAcc.pos

added def Ordinal.IsAcc

added theorem Ordinal.IsClosedBelow.iInter

added theorem Ordinal.IsClosedBelow.sInter

added def Ordinal.IsClosedBelow

added theorem Ordinal.accPt_subtype

added theorem Ordinal.isAcc_iff

added theorem Ordinal.isClosedBelow_iff

Modified Mathlib/Topology/Basic.lean

added theorem clusterPt_principal