Cardinalities of predicate extensions #
Mirror of Mathlib/Data/Set/Card.lean: on a finite type the Set.ncard of a predicate's
extension is the cardinality of its Finset filter, at any decidability instance, so a
statement about Set.ncard evaluates by decide. [UPSTREAM]
theorem
Set.ncard_setOf_eq_card_filter
{α : Type u_1}
[Fintype α]
(p : α → Prop)
[DecidablePred p]
:
{x : α | p x}.ncard = (Finset.filter p Finset.univ).card
On a finite type the extension of a predicate has the cardinality of its Finset filter.
[UPSTREAM]