[Merged by Bors] - feat: club sets#37677
Conversation
github-actions
Bot
added
the
large-import
PR summary cb72a58dcdImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
| cases topOrderOrNoTopOrder α | ||
| · exact .sInter_of_orderTop hs | ||
| · cases one_lt_cof.not_ge hα |
There was a problem hiding this comment.
Can you abstract this out into a lemma saying that cof alpha <= 1 -> Nonempty (OrderTop alpha)? Also, topOrderOrNoTopOrder looks misnamed, but that's pre-existing I guess.
There was a problem hiding this comment.
We already have this (the correct version of it, at least): cof_eq_one_iff.
Agree with the other theorem being misnamed, I'll open a PR for that later tonight.
There was a problem hiding this comment.
Why not use it here then? Is it impractical?
There was a problem hiding this comment.
If you have golfing ideas, let me know! This is as short as I could get it.
YaelDillies
added
the
awaiting-author
vihdzp
removed
the
awaiting-author
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! 🚀
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
mathlib-triage
Bot
added
the
maintainer-merge
| variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α] | ||
|
|
||
| @[simp] | ||
| theorem IsClub.of_isEmpty [IsEmpty α] {s : Set α} : IsClub s := |
There was a problem hiding this comment.
Can you just namespace IsClub instead for this file (the last two declarations will need _root_.)
There was a problem hiding this comment.
Really sorry, I did this locally but forgot to push. I opened #39641 to implement this change.
|
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
mathlib-triage
Bot
added
delegated
|
bors r+ |
In set theory, a club set is a subset of an ordinal of uncountable cofinality, which is closed in the order topology, and unbounded within the ordinal. We generalize this notion to that of a club set in a well-order `α`: this is a set which is cofinal and closed under suprema. We recover the more standard notion by setting `α = Iio o`, whenever `ℵ₀ < o.cof`. We prove that club sets are closed under intersections of size less than the cofinality of `α`, and that the fixed points of a normal function are a club set.
|
Pull request successfully merged into master. Build succeeded:
|
In set theory, a club set is a subset of an ordinal of uncountable cofinality, which is closed in the order topology, and unbounded within the ordinal. We generalize this notion to that of a club set in a well-order `α`: this is a set which is cofinal and closed under suprema. We recover the more standard notion by setting `α = Iio o`, whenever `ℵ₀ < o.cof`. We prove that club sets are closed under intersections of size less than the cofinality of `α`, and that the fixed points of a normal function are a club set.
In set theory, a club set is a subset of an ordinal of uncountable cofinality, which is closed in the order topology, and unbounded within the ordinal. We generalize this notion to that of a club set in a well-order `α`: this is a set which is cofinal and closed under suprema. We recover the more standard notion by setting `α = Iio o`, whenever `ℵ₀ < o.cof`. We prove that club sets are closed under intersections of size less than the cofinality of `α`, and that the fixed points of a normal function are a club set.
…over-community#39641) I meant to do this in leanprover-community#37677, but forgot to do `git push`.
In set theory, a club set is a subset of an ordinal of uncountable cofinality, which is closed in the order topology, and unbounded within the ordinal. We generalize this notion to that of a club set in a well-order `α`: this is a set which is cofinal and closed under suprema. We recover the more standard notion by setting `α = Iio o`, whenever `ℵ₀ < o.cof`. We prove that club sets are closed under intersections of size less than the cofinality of `α`, and that the fixed points of a normal function are a club set.
…over-community#39641) I meant to do this in leanprover-community#37677, but forgot to do `git push`.
4 participants
In set theory, a club set is a subset of an ordinal of uncountable cofinality, which is closed in the order topology, and unbounded within the ordinal.
We generalize this notion to that of a club set in a well-order
α: this is a set which is cofinal and closed under suprema. We recover the more standard notion by settingα = Iio o, wheneverℵ₀ < o.cof.We prove that club sets are closed under intersections of size less than the cofinality of
α, and that the fixed points of a normal function are a club set.The idea is to eventually rework
Ordinal.deriv. This is simply the enumerator function for the fixed points off, and enumerator functions for club sets are always normal.DirSupClosed#37670