Cardinality of a finite set #
This defines the cardinality of a finset
and provides induction principles for finsets.
Main declarations #
finset.card
:s.card : ℕ
returns the cardinality ofs : finset α
.
Induction principles #
finset.strong_induction
: Strong inductionfinset.strong_induction_on
finset.strong_downward_induction
finset.strong_downward_induction_on
finset.case_strong_induction_on
TODO #
Should we add a noncomputable version?
s.card
is the number of elements of s
, aka its cardinality.
Equations
- s.card = ⇑multiset.card s.val
Alias of the reverse direction of finset.card_pos
.
If a ∈ s
is known, see also finset.card_insert_of_mem
and finset.card_insert_of_not_mem
.
If a ∈ s
is known, see also finset.card_erase_of_mem
and finset.erase_eq_of_not_mem
.
Lattice structure #
Explicit description of a finset from its card #
A finset
of a subsingleton type has cardinality at most one.
Inductions #
Suppose that, given objects defined on all strict subsets of any finset s
, one knows how to
define an object on s
. Then one can inductively define an object on all finsets, starting from
the empty set and iterating. This can be used either to define data, or to prove properties.
Equations
- finset.strong_induction H s = H s (λ (t : finset α) (h : t ⊂ s), finset.strong_induction H t)
Analogue of strong_induction
with order of arguments swapped.
Equations
- s.strong_induction_on = λ (H : Π (s : finset α), (Π (t : finset α), t ⊂ s → p t) → p s), finset.strong_induction H s
Suppose that, given that p t
can be defined on all supersets of s
of cardinality less than
n
, one knows how to define p s
. Then one can inductively define p s
for all finsets s
of
cardinality less than n
, starting from finsets of card n
and iterating. This
can be used either to define data, or to prove properties.
Equations
- finset.strong_downward_induction H s = H s (λ (t : finset α) (ht : t.card ≤ n) (h : s ⊂ t), finset.strong_downward_induction H t ht)