-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: Finset of arbitrary size in an infinite type #8348
Conversation
and a few other easy lemmas
@@ -1651,6 +1667,14 @@ end Set | |||
|
|||
namespace Finset | |||
|
|||
lemma exists_card_eq [Infinite α] : ∀ n : ℕ, ∃ s : Finset α, s.card = n |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does this come from the fact that Tendsto Finset.card atTop atTop
in some way? Or, can this make the proof of that easier?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Kind of? You would then need to use Finset.exists_intermediate
to go from an arbitrary size finset back to the size you want. Certainly it doesn't look like an easier proof.
bors r+ |
and a few other easy lemmas
Pull request successfully merged into master. Build succeeded: |
and a few other easy lemmas
and a few other easy lemmas
and a few other easy lemmas