-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/set/ncard): noncomputable set cardinality #18576
Conversation
({a} : set α).ncard = 1 := | ||
by simp [ncard_eq_to_finset_card] | ||
|
||
lemma ncard_singleton_inter : ({a} ∩ s).ncard ≤ 1 := |
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.
Might be best to first prove a subsingleton set has cardinality ≤1, then use that a subsingleton subset is a subsingleton.
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.
LGTM, thanks!
Let's just wait for @kmill to have a look (who knows finite set in Lean better than me).
I think it's reasonable to merge this, we can always change it later if needed, thanks! bors merge |
This PR introduces a function `set.ncard` that (noncomputably) gives the cardinality of a finite `set`, or zero if the set is infinite. The intention is to give a way to reason about set cardinality that avoids data and going between `set` and `finset`. This is especially useful for reasoning about sets in a `finite` type. The added file is somewhat large, but it is essentially just duplicating the API in `data.finset.card` (minus the induction lemmas). Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This PR introduces a function
set.ncard
that (noncomputably) gives the cardinality of a finiteset
, or zero if the set is infinite. The intention is to give a way to reason about set cardinality that avoids data and going betweenset
andfinset
. This is especially useful for reasoning about sets in afinite
type.The added file is somewhat large, but it is essentially just duplicating the API in
data.finset.card
(minus the induction lemmas).