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 #
Alias of the reverse direction of Finset.card_pos
.
Alias of the reverse direction of Finset.card_ne_zero
.
If a ∈ s
is known, see also Finset.card_insert_of_mem
and Finset.card_insert_of_not_mem
.
Alias of Finset.card_pair
.
$\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$.
$\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$.
This result is casted to any additive group with 1,
so that we don't have to work with ℕ
-subtraction.
If a ∈ s
is known, see also Finset.card_erase_of_mem
and Finset.erase_eq_of_not_mem
.
Reorder a finset.
The difference with Finset.card_bij'
is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with Finset.card_nbij
is that the bijection is allowed to use membership of the
domain, rather than being a non-dependent function.
Alias of Finset.card_bij
.
Reorder a finset.
The difference with Finset.card_bij'
is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with Finset.card_nbij
is that the bijection is allowed to use membership of the
domain, rather than being a non-dependent function.
Reorder a finset.
The difference with Finset.card_bij
is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with Finset.card_nbij'
is that the bijection and its inverse are allowed to use
membership of the domains, rather than being non-dependent functions.
Reorder a finset.
The difference with Finset.card_nbij'
is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with Finset.card_bij
is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain.
Reorder a finset.
The difference with Finset.card_nbij
is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with Finset.card_bij'
is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains.
The difference with Finset.card_equiv
is that bijectivity is only required to hold on the domains,
rather than on the entire types.
Specialization of Finset.card_nbij'
that automatically fills in most arguments.
See Fintype.card_equiv
for the version where s
and t
are univ
.
Specialization of Finset.card_nbij
that automatically fills in most arguments.
See Fintype.card_bijective
for the version where s
and t
are univ
.
Alias of Finset.card_le_card_of_injOn
.
Lattice structure #
Alias of the reverse direction of Finset.card_union_eq_card_add_card
.
Alias of the reverse direction of Finset.card_union_eq_card_add_card
.
Alias of the reverse direction of Finset.card_union_eq_card_add_card
.
Alias of the reverse direction of Finset.card_union_eq_card_add_card
.
Alias of the reverse direction of Finset.card_union_eq_card_add_card
.
Given a subset s
of a set t
, of sizes at most and at least n
respectively, there exists a
set u
of size n
which is both a superset of s
and a subset of t
.
Explicit description of a finset from its card #
A Finset
of a subsingleton type has cardinality at most one.
Alias of Finset.one_lt_card_iff_nontrivial
.
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.
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.strongInduction H x = H x fun (t : Finset α) (h : t ⊂ x) => let_fun this := ⋯; Finset.strongInduction H t
Instances For
Analogue of strongInduction
with order of arguments swapped.
Equations
- s.strongInductionOn H = Finset.strongInduction H s
Instances For
Suppose that, given objects defined on all nonempty strict subsets of any nontrivial finset s
,
one knows how to define an object on s
. Then one can inductively define an object on all finsets,
starting from singletons and iterating.
TODO: Currently this can only be used to prove properties.
Replace Finset.Nonempty.exists_eq_singleton_or_nontrivial
with computational content
in order to let p
be Sort
-valued.
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.strongDownwardInduction H x = H x fun {t : Finset α} (ht : t.card ≤ n) (h : x ⊂ t) => let_fun this := ⋯; let_fun this := ⋯; Finset.strongDownwardInduction H t ht
Instances For
Analogue of strongDownwardInduction
with order of arguments swapped.
Equations
- s.strongDownwardInductionOn H = Finset.strongDownwardInduction H s