-
Notifications
You must be signed in to change notification settings - Fork 299
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(set_theory/cardinal/basic): lemmas about #(finset α)
#14850
Conversation
lemma mk_finset {α : Type u} {s : finset α} : #s = ↑(finset.card s) := by simp | ||
lemma mk_of_finset {α : Type u} {s : finset α} : #s = ↑(finset.card s) := by simp | ||
|
||
lemma mk_finset_of_fintype [fintype α] : #(finset α) = 2 ^ℕ fintype.card α := by simp |
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.
Can you squeeze this simp, for the sake of making it clear which lemmas this uses?
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.
This simp
basically just turns #(finset α)
into fintype.card (finset α)
, for which the lemma stating that it's equal to 2 ^ fintype.card α
already exists. A few other proofs in this file, like mk_fin
, mk_bool
, mk_Prop
, use this same technique and are not squeezed.
Should I squeeze it anyways?
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.
I think that non-squeezed simp
s are OK as long as they're fast.
Thanks! |
This PR does the following: - prove `mk_finset_of_fintype : #(finset α) = 2 ^ℕ fintype.card α` for `fintype α` - rename `mk_finset_eq_mk` to `mk_finset_of_infinite` to match the former - rename `mk_finset` to `mk_coe_finset` to avoid confusion with these two lemmas
Pull request successfully merged into master. Build succeeded: |
#(finset α)
#(finset α)
This PR does the following: - prove `mk_finset_of_fintype : #(finset α) = 2 ^ℕ fintype.card α` for `fintype α` - rename `mk_finset_eq_mk` to `mk_finset_of_infinite` to match the former - rename `mk_finset` to `mk_coe_finset` to avoid confusion with these two lemmas
This PR does the following:
mk_finset_of_fintype : #(finset α) = 2 ^ℕ fintype.card α
forfintype α
mk_finset_eq_mk
tomk_finset_of_infinite
to match the formermk_finset
tomk_coe_finset
to avoid confusion with these two lemmas