Cardinality of a finite set #
This defines the cardinality of a Finset
and provides induction principles for finsets.
Main declarations #
Finset.card
:#s : ℕ
returns the cardinality ofs : Finset α
.
Induction principles #
s.card
is the number of elements of s
, aka its cardinality.
The notation #s
can be accessed in the Finset
locale.
Equations
- Finset.«term#_» = Lean.ParserDescr.node `Finset.«term#_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1023))
Instances For
Alias of the reverse direction of Finset.card_pos
.
Alias of the reverse direction of Finset.card_ne_zero
.
Alias of Finset.card_insert_of_notMem
.
If a ∈ s
is known, see also Finset.card_insert_of_mem
and Finset.card_insert_of_notMem
.
If a ∈ s
is known, see also Finset.card_erase_of_mem
and Finset.erase_eq_of_notMem
.
Alias of the forward direction of Finset.card_filter_eq_iff
.
See also card_bij
.
TODO: consider deprecating, since this has been unused in mathlib for a long time and is just a
special case of card_bij
.
Given a bijection from a finite set s
to a finite set t
, the cardinalities of s
and t
are equal.
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.
Given a bijection from a finite set s
to a finite set t
, the cardinalities of s
and t
are equal.
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.
Given a bijection from a finite set s
to a finite set t
, the cardinalities of s
and t
are equal.
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.
Given a bijection from a finite set s
to a finite set t
, the cardinalities of s
and t
are equal.
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
.
If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole.
See also Finset.card_le_card_of_injOn
, which is a more general version of this lemma.
TODO: consider deprecating, since this is just a special case of Finset.card_le_card_of_injOn
.
Given an injective map f
from a finite set s
to another finite set t
, if t
is no larger
than s
, then f
is surjective to t
when restricted to s
.
See Finset.surj_on_of_inj_on_of_card_le
for the version where f
is a dependent function.
Given an injective map f
defined on a finite set s
to another finite set t
, if t
is no
larger than s
, then f
is surjective to t
when restricted to s
.
See Finset.surjOn_of_injOn_of_card_le
for the version where f
is a non-dependent function.
Given a surjectiive map f
from a finite set s
to another finite set t
, if s
is no larger
than t
, then f
is injective when restricted to s
.
See Finset.inj_on_of_surj_on_of_card_le
for the version where f
is a dependent function.
Given a surjective map f
defined on a finite set s
to another finite set t
, if s
is no
larger than t
, then f
is injective when restricted to s
.
See Finset.injOn_of_surjOn_of_card_le
for the version where f
is a non-dependent function.
Lattice structure #
Alias of the reverse direction of Finset.card_union_eq_card_add_card
.
Alias of Finset.exists_mem_notMem_of_card_lt_card
.
Alias of the reverse direction of Finset.card_sdiff_eq_card_sdiff_iff
.
Explicit description of a finset from its card #
A Finset
of a subsingleton type has cardinality at most one.
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✝) => have 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) => have this := ⋯; have this := ⋯; Finset.strongDownwardInduction H t ht
Instances For
To prove a proposition for an arbitrary Finset α
,
it suffices to prove that for any S : Finset α
, the following is true:
the property is true for S with any element s
removed, then the property holds for S
.
This is a weaker version of Finset.strongInduction
.
But it can be more precise when the induction argument
only requires removing single elements at a time.