mathlibdocumentation

data.fintype.card

Cardinalities of finite types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations #

• `fintype.card α`: Cardinality of a fintype. Equal to `finset.univ.card`.
• `fintype.trunc_equiv_fin`: A fintype `α` is computably equivalent to `fin (card α)`. The `trunc`-free, noncomputable version is `fintype.equiv_fin`.
• `fintype.trunc_equiv_of_card_eq` `fintype.equiv_of_card_eq`: Two fintypes of same cardinality are equivalent. See above.
• `fin.equiv_iff_eq`: `fin m ≃ fin n` iff `m = n`.
• `infinite.nat_embedding`: An embedding of `ℕ` into an infinite type.

We also provide the following versions of the pigeonholes principle.

• `fintype.exists_ne_map_eq_of_card_lt` and `is_empty_of_card_lt`: Finitely many pigeons and pigeonholes. Weak formulation.
• `finite.exists_ne_map_eq_of_infinite`: Infinitely many pigeons in finitely many pigeonholes. Weak formulation.
• `finite.exists_infinite_fiber`: Infinitely many pigeons in finitely many pigeonholes. Strong formulation.

Some more pigeonhole-like statements can be found in `data.fintype.card_embedding`.

Types which have an injection from/a surjection to an `infinite` type are themselves `infinite`. See `infinite.of_injective` and `infinite.of_surjective`.

Instances #

We provide `infinite` instances for

• specific types: `ℕ`, `ℤ`
• type constructors: `multiset α`, `list α`
def fintype.card (α : Type u_1) [fintype α] :

`card α` is the number of elements in `α`, defined when `α` is a fintype.

Equations
def fintype.trunc_equiv_fin (α : Type u_1) [decidable_eq α] [fintype α] :

There is (computably) an equivalence between `α` and `fin (card α)`.

Since it is not unique and depends on which permutation of the universe list is used, the equivalence is wrapped in `trunc` to preserve computability.

See `fintype.equiv_fin` for the noncomputable version, and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq` for an equiv `α ≃ fin n` given `fintype.card α = n`.

See `fintype.trunc_fin_bijection` for a version without `[decidable_eq α]`.

Equations
noncomputable def fintype.equiv_fin (α : Type u_1) [fintype α] :

There is (noncomputably) an equivalence between `α` and `fin (card α)`.

See `fintype.trunc_equiv_fin` for the computable version, and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq` for an equiv `α ≃ fin n` given `fintype.card α = n`.

Equations
• = let _inst : := in
def fintype.trunc_fin_bijection (α : Type u_1) [fintype α] :
trunc {f //

There is (computably) a bijection between `fin (card α)` and `α`.

Since it is not unique and depends on which permutation of the universe list is used, the bijection is wrapped in `trunc` to preserve computability.

See `fintype.trunc_equiv_fin` for a version that gives an equivalence given `[decidable_eq α]`.

Equations
theorem fintype.subtype_card {α : Type u_1} {p : α Prop} (s : finset α) (H : (x : α), x s p x) :
fintype.card {x // p x} = s.card
theorem fintype.card_of_subtype {α : Type u_1} {p : α Prop} (s : finset α) (H : (x : α), x s p x) [fintype {x // p x}] :
fintype.card {x // p x} = s.card
@[simp]
theorem fintype.card_of_finset {α : Type u_1} {p : set α} (s : finset α) (H : (x : α), x s x p) :
theorem fintype.card_of_finset' {α : Type u_1} {p : set α} (s : finset α) (H : (x : α), x s x p) [fintype p] :
theorem fintype.of_equiv_card {α : Type u_1} {β : Type u_2} [fintype α] (f : α β) :
theorem fintype.card_congr {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) :
theorem fintype.card_congr' {α β : Type u_1} [fintype α] [fintype β] (h : α = β) :
def fintype.trunc_equiv_fin_of_card_eq {α : Type u_1} [fintype α] [decidable_eq α] {n : } (h : = n) :
trunc fin n)

If the cardinality of `α` is `n`, there is computably a bijection between `α` and `fin n`.

See `fintype.equiv_fin_of_card_eq` for the noncomputable definition, and `fintype.trunc_equiv_fin` and `fintype.equiv_fin` for the bijection `α ≃ fin (card α)`.

Equations
noncomputable def fintype.equiv_fin_of_card_eq {α : Type u_1} [fintype α] {n : } (h : = n) :
α fin n

If the cardinality of `α` is `n`, there is noncomputably a bijection between `α` and `fin n`.

See `fintype.trunc_equiv_fin_of_card_eq` for the computable definition, and `fintype.trunc_equiv_fin` and `fintype.equiv_fin` for the bijection `α ≃ fin (card α)`.

Equations
• = let _inst : := in
def fintype.trunc_equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] (h : = ) :
trunc β)

Two `fintype`s with the same cardinality are (computably) in bijection.

See `fintype.equiv_of_card_eq` for the noncomputable version, and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq` for the specialization to `fin`.

Equations
noncomputable def fintype.equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : = ) :
α β

Two `fintype`s with the same cardinality are (noncomputably) in bijection.

See `fintype.trunc_equiv_of_card_eq` for the computable version, and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq` for the specialization to `fin`.

Equations
• = let _inst : := , _inst_3 : := in
theorem fintype.card_eq {α : Type u_1} {β : Type u_2} [F : fintype α] [G : fintype β] :
nonempty β)
@[simp]
theorem fintype.card_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

Note: this lemma is specifically about `fintype.of_subsingleton`. For a statement about arbitrary `fintype` instances, use either `fintype.card_le_one_iff_subsingleton` or `fintype.card_unique`.

@[simp]
theorem fintype.card_unique {α : Type u_1} [unique α] [h : fintype α] :
@[simp]
theorem fintype.card_of_is_empty {α : Type u_1} [is_empty α] :

Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about arbitrary `fintype` instances, use `fintype.card_eq_zero_iff`.

@[simp]
theorem set.to_finset_card {α : Type u_1} (s : set α) [fintype s] :
theorem finset.card_univ {α : Type u_1} [fintype α] :
theorem finset.eq_univ_of_card {α : Type u_1} [fintype α] (s : finset α) (hs : s.card = ) :
theorem finset.card_eq_iff_eq_univ {α : Type u_1} [fintype α] (s : finset α) :
theorem finset.card_le_univ {α : Type u_1} [fintype α] (s : finset α) :
theorem finset.card_lt_univ_of_not_mem {α : Type u_1} [fintype α] {s : finset α} {x : α} (hx : x s) :
theorem finset.card_lt_iff_ne_univ {α : Type u_1} [fintype α] (s : finset α) :
theorem finset.card_univ_diff {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :
theorem finset.card_compl {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :
theorem fintype.card_compl_set {α : Type u_1} [fintype α] (s : set α) [fintype s] [fintype s] :
@[simp]
theorem fintype.card_fin (n : ) :
@[simp]
theorem finset.card_fin (n : ) :
theorem fin_injective  :

`fin` as a map from `ℕ` to `Type` is injective. Note that since this is a statement about equality of types, using it should be avoided if possible.

theorem fin.cast_eq_cast' {n m : } (h : fin n = fin m) :

A reversed version of `fin.cast_eq_cast` that is easier to rewrite with.

theorem card_finset_fin_le {n : } (s : finset (fin n)) :
s.card n
theorem fin.equiv_iff_eq {m n : } :
nonempty (fin m fin n) m = n
@[simp]
theorem fintype.card_subtype_eq {α : Type u_1} (y : α) [fintype {x // x = y}] :
fintype.card {x // x = y} = 1
@[simp]
theorem fintype.card_subtype_eq' {α : Type u_1} (y : α) [fintype {x // y = x}] :
fintype.card {x // y = x} = 1
@[simp]
theorem fintype.card_empty  :
@[simp]
theorem fintype.card_pempty  :
@[simp]
theorem fintype.card_punit  :
@[simp]
theorem fintype.card_bool  :
@[simp]
theorem fintype.card_ulift (α : Type u_1) [fintype α] :
@[simp]
theorem fintype.card_plift (α : Type u_1) [fintype α] :
@[simp]
theorem fintype.card_order_dual (α : Type u_1) [fintype α] :
@[simp]
theorem fintype.card_lex (α : Type u_1) [fintype α] :
noncomputable def fintype.sum_left {α : Type u_1} {β : Type u_2} [fintype β)] :

Given that `α ⊕ β` is a fintype, `α` is also a fintype. This is non-computable as it uses that `sum.inl` is an injection, but there's no clear inverse if `α` is empty.

Equations
noncomputable def fintype.sum_right {α : Type u_1} {β : Type u_2} [fintype β)] :

Given that `α ⊕ β` is a fintype, `β` is also a fintype. This is non-computable as it uses that `sum.inr` is an injection, but there's no clear inverse if `β` is empty.

Equations

Relation to `finite`#

In this section we prove that `α : Type*` is `finite` if and only if `fintype α` is nonempty.

@[protected, nolint]
theorem fintype.finite {α : Type u_1} (h : fintype α) :
@[protected, nolint, instance]
def finite.of_fintype (α : Type u_1) [fintype α] :

For efficiency reasons, we want `finite` instances to have higher priority than ones coming from `fintype` instances.

theorem nonempty_fintype (α : Type u_1) [finite α] :

See also `nonempty_encodable`, `nonempty_denumerable`.

noncomputable def fintype.of_finite (α : Type u_1) [finite α] :

Noncomputably get a `fintype` instance from a `finite` instance. This is not an instance because we want `fintype` instances to be useful for computations.

Equations
theorem finite.of_injective {α : Sort u_1} {β : Sort u_2} [finite β] (f : α β) (H : function.injective f) :
theorem finite.of_surjective {α : Sort u_1} {β : Sort u_2} [finite α] (f : α β) (H : function.surjective f) :
theorem finite.exists_univ_list (α : Type u_1) [finite α] :
(l : list α), l.nodup (x : α), x l
theorem list.nodup.length_le_card {α : Type u_1} [fintype α] {l : list α} (h : l.nodup) :
theorem fintype.card_le_of_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) (hf : function.injective f) :
theorem fintype.card_le_of_embedding {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) :
theorem fintype.card_lt_of_injective_of_not_mem {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) (h : function.injective f) {b : β} (w : b ) :
theorem fintype.card_lt_of_injective_not_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) (h : function.injective f) (h' : ¬) :
theorem fintype.card_le_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) (h : function.surjective f) :
theorem fintype.card_range_le {α : Type u_1} {β : Type u_2} (f : α β) [fintype α] [fintype (set.range f)] :
theorem fintype.card_range {α : Type u_1} {β : Type u_2} {F : Type u_3} [ β] (f : F) [fintype α] [fintype (set.range f)] :
theorem fintype.exists_ne_map_eq_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) (h : < ) :
(x y : α), x y f x = f y

The pigeonhole principle for finitely many pigeons and pigeonholes. This is the `fintype` version of `finset.exists_ne_map_eq_of_card_lt_of_maps_to`.

theorem fintype.card_eq_one_iff {α : Type u_1} [fintype α] :
(x : α), (y : α), y = x
theorem fintype.card_eq_zero_iff {α : Type u_1} [fintype α] :
theorem fintype.card_eq_zero {α : Type u_1} [fintype α] [is_empty α] :

A `fintype` with cardinality zero is equivalent to `empty`.

Equations
theorem fintype.card_pos_iff {α : Type u_1} [fintype α] :
theorem fintype.card_pos {α : Type u_1} [fintype α] [h : nonempty α] :
theorem fintype.card_ne_zero {α : Type u_1} [fintype α] [nonempty α] :
theorem fintype.card_le_one_iff {α : Type u_1} [fintype α] :
(a b : α), a = b
theorem fintype.exists_ne_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < ) (a : α) :
(b : α), b a
theorem fintype.exists_pair_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < ) :
(a b : α), a b
theorem fintype.card_eq_one_of_forall_eq {α : Type u_1} [fintype α] {i : α} (h : (j : α), j = i) :
theorem fintype.one_lt_card {α : Type u_1} [fintype α] [h : nontrivial α] :
theorem fintype.one_lt_card_iff {α : Type u_1} [fintype α] :
(a b : α), a b
theorem fintype.two_lt_card_iff {α : Type u_1} [fintype α] :
(a b c : α), a b a c b c
theorem fintype.card_of_bijective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α β} (hf : function.bijective f) :
theorem finite.injective_iff_surjective {α : Type u_1} [finite α] {f : α α} :
theorem finite.injective_iff_bijective {α : Type u_1} [finite α] {f : α α} :
theorem finite.surjective_iff_bijective {α : Type u_1} [finite α] {f : α α} :
theorem finite.injective_iff_surjective_of_equiv {α : Type u_1} {β : Type u_2} [finite α] {f : α β} (e : α β) :
theorem function.injective.bijective_of_finite {α : Type u_1} [finite α] {f : α α} :

Alias of the forward direction of `finite.injective_iff_bijective`.

theorem function.surjective.bijective_of_finite {α : Type u_1} [finite α] {f : α α} :

Alias of the forward direction of `finite.surjective_iff_bijective`.

theorem function.injective.surjective_of_fintype {α : Type u_1} {β : Type u_2} [finite α] {f : α β} (e : α β) :

Alias of the forward direction of `finite.injective_iff_surjective_of_equiv`.

theorem function.surjective.injective_of_fintype {α : Type u_1} {β : Type u_2} [finite α] {f : α β} (e : α β) :

Alias of the reverse direction of `finite.injective_iff_surjective_of_equiv`.

theorem fintype.bijective_iff_injective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) :
theorem fintype.bijective_iff_surjective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) :
theorem function.left_inverse.right_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α β} {g : β α} (hfg : g) (hcard : ) :
theorem function.right_inverse.left_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α β} {g : β α} (hfg : g) (hcard : ) :
def equiv.of_left_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : ) (f : α β) (g : β α) (h : f) :
α β

Construct an equivalence from functions that are inverse to each other.

Equations
@[simp]
theorem equiv.of_left_inverse_of_card_le_symm_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : ) (f : α β) (g : β α) (h : f) (ᾰ : β) :
g h).symm) = g ᾰ
@[simp]
theorem equiv.of_left_inverse_of_card_le_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : ) (f : α β) (g : β α) (h : f) (ᾰ : α) :
g h) = f ᾰ
def equiv.of_right_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : ) (f : α β) (g : β α) (h : f) :
α β

Construct an equivalence from functions that are inverse to each other.

Equations
@[simp]
theorem equiv.of_right_inverse_of_card_le_symm_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : ) (f : α β) (g : β α) (h : f) (ᾰ : β) :
g h).symm) = g ᾰ
@[simp]
theorem equiv.of_right_inverse_of_card_le_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : ) (f : α β) (g : β α) (h : f) (ᾰ : α) :
h) = f ᾰ
@[simp]
theorem fintype.card_coe {α : Type u_1} (s : finset α) [fintype s] :
noncomputable def finset.equiv_fin {α : Type u_1} (s : finset α) :

Noncomputable equivalence between a finset `s` coerced to a type and `fin s.card`.

Equations
noncomputable def finset.equiv_fin_of_card_eq {α : Type u_1} {s : finset α} {n : } (h : s.card = n) :

Noncomputable equivalence between a finset `s` as a fintype and `fin n`, when there is a proof that `s.card = n`.

Equations
noncomputable def finset.equiv_of_card_eq {α : Type u_1} {s t : finset α} (h : s.card = t.card) :

Noncomputable equivalence between two finsets `s` and `t` as fintypes when there is a proof that `s.card = t.card`.

Equations
@[simp]
theorem fintype.card_Prop  :
theorem set_fintype_card_le_univ {α : Type u_1} [fintype α] (s : set α) [fintype s] :
theorem set_fintype_card_eq_univ_iff {α : Type u_1} [fintype α] (s : set α) [fintype s] :
noncomputable def function.embedding.equiv_of_fintype_self_embedding {α : Type u_1} [finite α] (e : α α) :
α α

An embedding from a `fintype` to itself can be promoted to an equivalence.

Equations
@[simp]
theorem function.embedding.is_empty_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : < ) :
is_empty β)

If `‖β‖ < ‖α‖` there are no embeddings `α ↪ β`. This is a formulation of the pigeonhole principle.

Note this cannot be an instance as it needs `h`.

def function.embedding.trunc_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] (h : ) :
trunc β)

A constructive embedding of a fintype `α` in another fintype `β` when `card α ≤ card β`.

Equations
theorem function.embedding.nonempty_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : ) :
nonempty β)
theorem function.embedding.nonempty_iff_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
nonempty β)
theorem function.embedding.exists_of_card_le_finset {α : Type u_1} {β : Type u_2} [fintype α] {s : finset β} (h : s.card) :
(f : α β), s
@[simp]
theorem finset.univ_map_embedding {α : Type u_1} [fintype α] (e : α α) :
theorem fintype.card_lt_of_surjective_not_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) (h : function.surjective f) (h' : ¬) :
theorem fintype.card_subtype_le {α : Type u_1} [fintype α] (p : α Prop)  :
fintype.card {x // p x}
theorem fintype.card_subtype_lt {α : Type u_1} [fintype α] {p : α Prop} {x : α} (hx : ¬p x) :
fintype.card {x // p x} <
theorem fintype.card_subtype {α : Type u_1} [fintype α] (p : α Prop)  :
fintype.card {x // p x} =
@[simp]
theorem fintype.card_subtype_compl {α : Type u_1} [fintype α] (p : α Prop) [fintype {x // p x}] [fintype {x // ¬p x}] :
fintype.card {x // ¬p x} = - fintype.card {x // p x}
theorem fintype.card_subtype_mono {α : Type u_1} (p q : α Prop) (h : p q) [fintype {x // p x}] [fintype {x // q x}] :
fintype.card {x // p x} fintype.card {x // q x}
theorem fintype.card_compl_eq_card_compl {α : Type u_1} [finite α] (p q : α Prop) [fintype {x // p x}] [fintype {x // ¬p x}] [fintype {x // q x}] [fintype {x // ¬q x}] (h : fintype.card {x // p x} = fintype.card {x // q x}) :
fintype.card {x // ¬p x} = fintype.card {x // ¬q x}

If two subtypes of a fintype have equal cardinality, so do their complements.

theorem fintype.card_quotient_le {α : Type u_1} [fintype α] (s : setoid α)  :
theorem fintype.card_quotient_lt {α : Type u_1} [fintype α] {s : setoid α} {x y : α} (h1 : x y) (h2 : x y) :
theorem univ_eq_singleton_of_card_one {α : Type u_1} [fintype α] (x : α) (h : = 1) :
theorem finite.well_founded_of_trans_of_irrefl {α : Type u_1} [finite α] (r : α α Prop) [ r] [ r] :
theorem finite.preorder.well_founded_lt {α : Type u_1} [finite α] [preorder α] :
theorem finite.preorder.well_founded_gt {α : Type u_1} [finite α] [preorder α] :
@[protected, instance]
@[protected, instance]
@[protected, nolint]
theorem fintype.false {α : Type u_1} [infinite α] (h : fintype α) :
@[simp]
theorem is_empty_fintype {α : Type u_1} :
noncomputable def fintype_of_not_infinite {α : Type u_1} (h : ¬) :

A non-infinite type is a fintype.

Equations
noncomputable def fintype_or_infinite (α : Type u_1) :

Any type is (classically) either a `fintype`, or `infinite`.

One can obtain the relevant typeclasses via `cases fintype_or_infinite α; resetI`.

Equations
theorem finset.exists_minimal {α : Type u_1} [preorder α] (s : finset α) (h : s.nonempty) :
(m : α) (H : m s), (x : α), x s ¬x < m
theorem finset.exists_maximal {α : Type u_1} [preorder α] (s : finset α) (h : s.nonempty) :
(m : α) (H : m s), (x : α), x s ¬m < x
theorem infinite.of_not_fintype {α : Type u_1} (h : false) :
theorem infinite.of_injective_to_set {α : Type u_1} {s : set α} (hs : s set.univ) {f : α s} (hf : function.injective f) :

If `s : set α` is a proper subset of `α` and `f : α → s` is injective, then `α` is infinite.

theorem infinite.of_surjective_from_set {α : Type u_1} {s : set α} (hs : s set.univ) {f : s α} (hf : function.surjective f) :

If `s : set α` is a proper subset of `α` and `f : s → α` is surjective, then `α` is infinite.

theorem infinite.exists_not_mem_finset {α : Type u_1} [infinite α] (s : finset α) :
(x : α), x s
@[protected, instance]
def infinite.nontrivial (α : Type u_1) [H : infinite α] :
@[protected]
theorem infinite.nonempty (α : Type u_1) [infinite α] :
theorem infinite.of_injective {α : Sort u_1} {β : Sort u_2} [infinite β] (f : β α) (hf : function.injective f) :
theorem infinite.of_surjective {α : Sort u_1} {β : Sort u_2} [infinite β] (f : α β) (hf : function.surjective f) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def multiset.infinite {α : Type u_1} [nonempty α] :
@[protected, instance]
def list.infinite {α : Type u_1} [nonempty α] :
@[protected, instance]
def infinite.set {α : Type u_1} [infinite α] :
@[protected, instance]
def finset.infinite {α : Type u_1} [infinite α] :
@[protected, instance]
def option.infinite {α : Type u_1} [infinite α] :
@[protected, instance]
def sum.infinite_of_left {α : Type u_1} {β : Type u_2} [infinite α] :
infinite β)
@[protected, instance]
def sum.infinite_of_right {α : Type u_1} {β : Type u_2} [infinite β] :
infinite β)
@[protected, instance]
def prod.infinite_of_right {α : Type u_1} {β : Type u_2} [nonempty α] [infinite β] :
infinite × β)
@[protected, instance]
def prod.infinite_of_left {α : Type u_1} {β : Type u_2} [infinite α] [nonempty β] :
infinite × β)
noncomputable def infinite.nat_embedding (α : Type u_1) [infinite α] :
α

Embedding of `ℕ` into an infinite type.

Equations
theorem infinite.exists_subset_card_eq (α : Type u_1) [infinite α] (n : ) :
(s : finset α), s.card = n

See `infinite.exists_superset_card_eq` for a version that, for a `s : finset α`, provides a superset `t : finset α`, `s ⊆ t` such that `t.card` is fixed.

theorem infinite.exists_superset_card_eq {α : Type u_1} [infinite α] (s : finset α) (n : ) (hn : s.card n) :
(t : finset α), s t t.card = n

See `infinite.exists_subset_card_eq` for a version that provides an arbitrary `s : finset α` for any cardinality.

noncomputable def fintype_of_finset_card_le {ι : Type u_1} (n : ) (w : (s : finset ι), s.card n) :

If every finset in a type has bounded cardinality, that type is finite.

Equations
theorem not_injective_infinite_finite {α : Sort u_1} {β : Sort u_2} [infinite α] [finite β] (f : α β) :
theorem finite.exists_ne_map_eq_of_infinite {α : Sort u_1} {β : Sort u_2} [infinite α] [finite β] (f : α β) :
(x y : α), x y f x = f y

The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the same pigeonhole.

See also: `fintype.exists_ne_map_eq_of_card_lt`, `finite.exists_infinite_fiber`.

@[protected, instance]
def function.embedding.is_empty {α : Sort u_1} {β : Sort u_2} [infinite α] [finite β] :
is_empty β)
theorem finite.exists_infinite_fiber {α : Type u_1} {β : Type u_2} [infinite α] [finite β] (f : α β) :
(y : β), infinite (f ⁻¹' {y})

The strong pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there is a pigeonhole with infinitely many pigeons.

See also: `finite.exists_ne_map_eq_of_infinite`

theorem not_surjective_finite_infinite {α : Sort u_1} {β : Sort u_2} [finite α] [infinite β] (f : α β) :
def trunc_of_card_pos {α : Type u_1} [fintype α] (h : 0 < ) :

A `fintype` with positive cardinality constructively contains an element.

Equations
• = let _inst : := _ in
theorem fintype.induction_subsingleton_or_nontrivial {P : Π (α : Type u_1) [_inst_1 : fintype α], Prop} (α : Type u_1) [fintype α] (hbase : (α : Type u_1) [_inst_3 : fintype α] [_inst_4 : , P α) (hstep : (α : Type u_1) [_inst_5 : fintype α] [_inst_6 : , ( (β : Type u_1) [_inst_7 : fintype β], P β) P α) :
P α

A custom induction principle for fintypes. The base case is a subsingleton type, and the induction step is for non-trivial types, and one can assume the hypothesis for smaller types (via `fintype.card`).

The major premise is `fintype α`, so to use this with the `induction` tactic you have to give a name to that instance and use that name.

Extension for the `positivity` tactic: `finset.card s` is positive if `s` is nonempty.