Cardinality of a finite set #
This defines the cardinality of a
Finset and provides induction principles for finsets.
Main declarations #
Induction principles #
Finset.strongInduction: Strong induction
Should we add a noncomputable version?
If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole.
Lattice structure #
Given a set
A and a set
B inside it, we can shrink
A to any appropriate size, and keep
Explicit description of a finset from its card #
If a Finset in a Pi type is nontrivial (has at least two elements), then its projection to some factor is nontrivial, and the fibers of the projection are proper subsets.
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.
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
cardinality less than
n, starting from finsets of card
n and iterating. This
can be used either to define data, or to prove properties.
strongDownwardInduction with order of arguments swapped.