Commit 2023-05-30 14:04 74c2af38
View on Github →feat(data/set/ncard): noncomputable set cardinality (#18576)
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).