Commit 2026-05-24 14:07 383a355f

View on Github →

chore(SetTheory/Cardinality/Cofinality/Club): use namespace (#39641) I meant to do this in #37677, but forgot to do git push.

Estimated changes

modified theorem IsClub.csSup_mem
deleted theorem IsClub.iInter
modified theorem IsClub.iInter_of_cof_le_one
modified theorem IsClub.iInter_of_orderTop
deleted theorem IsClub.inter
modified theorem IsClub.isLUB_mem
modified theorem IsClub.of_isEmpty
deleted theorem IsClub.sInter
modified theorem IsClub.sInter_of_cof_le_one
modified theorem IsClub.sInter_of_orderTop
deleted theorem IsClub.union
deleted theorem IsClub.univ
modified theorem Order.IsNormal.isClub_range