Commit 2026-06-21 22:46 914b89d9

View on Github →

feat: stationary sets (#39727) We define stationary sets as sets intersecting all club sets, and prove basic theorems about them.

Estimated changes

Modified Mathlib/Order/Cofinal.lean

added theorem IsCofinal.nonempty

Modified Mathlib/SetTheory/Cardinal/Cofinality/Club.lean

added theorem IsClub.iInter_of_countable

added theorem IsClub.isStationary

added theorem IsClub.sInter_of_countable

added theorem IsStationary.mono

added theorem IsStationary.nonempty

added theorem IsStationary.of_not_isCofinal_compl

added def IsStationary

added theorem isClub_empty_iff

added theorem isStationary_iUnion_iff

added theorem isStationary_iUnion_iff_of_cof_le_one

added theorem isStationary_iUnion_iff_of_countable

added theorem isStationary_iUnion_iff_of_orderTop

added theorem isStationary_sUnion_iff

added theorem isStationary_sUnion_iff_of_cof_le_one

added theorem isStationary_sUnion_iff_of_countable

added theorem isStationary_sUnion_iff_of_orderTop

added theorem isStationary_union_iff

added theorem isStationary_univ_iff

added theorem not_isStationary_empty

added theorem not_isStationary_iff

added theorem not_isStationary_of_isEmpty