mathlib3 documentation

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 #

We also provide the following versions of the pigeonholes principle.

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

source
def fintype.card (α : Type u_1) [fintype α] :
ℕ

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

Equations
source
def fintype.trunc_equiv_fin (α : Type u_1) [decidable_eq α] [fintype α] :
trunc (α ≃ fin (fintype.card α))

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
source
noncomputable def fintype.equiv_fin (α : Type u_1) [fintype α] :
α ≃ fin (fintype.card α)

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
source
def fintype.trunc_fin_bijection (α : Type u_1) [fintype α] :
trunc {f // function.bijective 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
source
theorem fintype.subtype_card {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ p x) :
fintype.card {x // p x} = s.card
source
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
source
@[simp]
theorem fintype.card_of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :
fintype.card ↥p = s.card
source
theorem fintype.card_of_finset' {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) [fintype ↥p] :
fintype.card ↥p = s.card
source
theorem fintype.of_equiv_card {α : Type u_1} {β : Type u_2} [fintype α] (f : α ≃ β) :
fintype.card β = fintype.card α
source
theorem fintype.card_congr {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α ≃ β) :
fintype.card α = fintype.card β
source
theorem fintype.card_congr' {α β : Type u_1} [fintype α] [fintype β] (h : α = β) :
fintype.card α = fintype.card β
source
def fintype.trunc_equiv_fin_of_card_eq {α : Type u_1} [fintype α] [decidable_eq α] {n : ℕ} (h : fintype.card α = 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
source
noncomputable def fintype.equiv_fin_of_card_eq {α : Type u_1} [fintype α] {n : ℕ} (h : fintype.card α = 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
source
def fintype.trunc_equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] (h : fintype.card α = fintype.card β) :
trunc (α ≃ β)

Two fintypes 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
source
noncomputable def fintype.equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : fintype.card α = fintype.card β) :
α ≃ β

Two fintypes 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
source
theorem fintype.card_eq {α : Type u_1} {β : Type u_2} [F : fintype α] [G : fintype β] :
fintype.card α = fintype.card β ↔ nonempty (α ≃ β)
source
@[simp]
theorem fintype.card_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :
fintype.card α = 1

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.

source
@[simp]
theorem fintype.card_unique {α : Type u_1} [unique α] [h : fintype α] :
fintype.card α = 1
source
@[simp]
theorem fintype.card_of_is_empty {α : Type u_1} [is_empty α] :
fintype.card α = 0

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

source
@[simp]
theorem set.to_finset_card {α : Type u_1} (s : set α) [fintype ↥s] :
s.to_finset.card = fintype.card ↥s
source
theorem finset.card_univ {α : Type u_1} [fintype α] :
finset.univ.card = fintype.card α
source
theorem finset.eq_univ_of_card {α : Type u_1} [fintype α] (s : finset α) (hs : s.card = fintype.card α) :
s = finset.univ
source
theorem finset.card_eq_iff_eq_univ {α : Type u_1} [fintype α] (s : finset α) :
s.card = fintype.card α ↔ s = finset.univ
source
theorem finset.card_le_univ {α : Type u_1} [fintype α] (s : finset α) :
s.card ≤ fintype.card α
source
theorem finset.card_lt_univ_of_not_mem {α : Type u_1} [fintype α] {s : finset α} {x : α} (hx : x ∉ s) :
s.card < fintype.card α
source
theorem finset.card_lt_iff_ne_univ {α : Type u_1} [fintype α] (s : finset α) :
s.card < fintype.card α ↔ s ≠ finset.univ
source
theorem finset.card_compl_lt_iff_nonempty {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
sᶜ.card < fintype.card α ↔ s.nonempty
source
theorem finset.card_univ_diff {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :
(finset.univ \ s).card = fintype.card α - s.card
source
theorem finset.card_compl {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :
sᶜ.card = fintype.card α - s.card
source
theorem fintype.card_compl_set {α : Type u_1} [fintype α] (s : set α) [fintype ↥s] [fintype ↥sᶜ] :
fintype.card ↥sᶜ = fintype.card α - fintype.card ↥s
source
@[simp]
theorem fintype.card_fin (n : ℕ) :
fintype.card (fin n) = n
source
@[simp]
theorem finset.card_fin (n : ℕ) :
finset.univ.card = n
source
theorem fin_injective  :
function.injective fin

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.

source
theorem fin.cast_eq_cast' {n m : ℕ} (h : fin n = fin m) :
cast h = ⇑(fin.cast _)

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

source
theorem card_finset_fin_le {n : ℕ} (s : finset (fin n)) :
s.card ≤ n
source
theorem fin.equiv_iff_eq {m n : ℕ} :
nonempty (fin m ≃ fin n) ↔ m = n
source
@[simp]
theorem fintype.card_subtype_eq {α : Type u_1} (y : α) [fintype {x // x = y}] :
fintype.card {x // x = y} = 1
source
@[simp]
theorem fintype.card_subtype_eq' {α : Type u_1} (y : α) [fintype {x // y = x}] :
fintype.card {x // y = x} = 1
source
@[simp]
theorem fintype.card_empty  :
fintype.card empty = 0
source
@[simp]
theorem fintype.card_pempty  :
fintype.card pempty = 0
source
theorem fintype.card_unit  :
fintype.card unit = 1
source
@[simp]
theorem fintype.card_punit  :
fintype.card punit = 1
source
@[simp]
theorem fintype.card_bool  :
fintype.card bool = 2
source
@[simp]
theorem fintype.card_ulift (α : Type u_1) [fintype α] :
fintype.card (ulift α) = fintype.card α
source
@[simp]
theorem fintype.card_plift (α : Type u_1) [fintype α] :
fintype.card (plift α) = fintype.card α
source
@[simp]
theorem fintype.card_order_dual (α : Type u_1) [fintype α] :
fintype.card αᵒᵈ = fintype.card α
source
@[simp]
theorem fintype.card_lex (α : Type u_1) [fintype α] :
fintype.card (lex α) = fintype.card α
source
noncomputable def fintype.sum_left {α : Type u_1} {β : Type u_2} [fintype (α ⊕ β)] :
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
source
noncomputable def fintype.sum_right {α : Type u_1} {β : Type u_2} [fintype (α ⊕ β)] :
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.

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

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

source
theorem finite_iff_nonempty_fintype (α : Type u_1) :
finite α ↔ nonempty (fintype α)
source
theorem nonempty_fintype (α : Type u_1) [finite α] :
nonempty (fintype α)

See also nonempty_encodable, nonempty_denumerable.

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

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
source
theorem finite.of_injective {α : Sort u_1} {β : Sort u_2} [finite β] (f : α → β) (H : function.injective f) :
finite α
source
theorem finite.of_surjective {α : Sort u_1} {β : Sort u_2} [finite α] (f : α → β) (H : function.surjective f) :
finite β
source
theorem finite.exists_univ_list (α : Type u_1) [finite α] :
∃ (l : list α), l.nodup ∧ ∀ (x : α), x ∈ l
source
theorem list.nodup.length_le_card {α : Type u_1} [fintype α] {l : list α} (h : l.nodup) :
l.length ≤ fintype.card α
source
theorem fintype.card_le_of_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (hf : function.injective f) :
fintype.card α ≤ fintype.card β
source
theorem fintype.card_le_of_embedding {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α ↪ β) :
fintype.card α ≤ fintype.card β
source
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 ∉ set.range f) :
fintype.card α < fintype.card β
source
theorem fintype.card_lt_of_injective_not_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.injective f) (h' : ¬function.surjective f) :
fintype.card α < fintype.card β
source
theorem fintype.card_le_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.surjective f) :
fintype.card β ≤ fintype.card α
source
theorem fintype.card_range_le {α : Type u_1} {β : Type u_2} (f : α → β) [fintype α] [fintype ↥(set.range f)] :
fintype.card ↥(set.range f) ≤ fintype.card α
source
theorem fintype.card_range {α : Type u_1} {β : Type u_2} {F : Type u_3} [embedding_like F α β] (f : F) [fintype α] [fintype ↥(set.range ⇑f)] :
fintype.card ↥(set.range ⇑f) = fintype.card α
source
theorem fintype.exists_ne_map_eq_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : fintype.card β < fintype.card α) :
∃ (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.

source
theorem fintype.card_eq_one_iff {α : Type u_1} [fintype α] :
fintype.card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x
source
theorem fintype.card_eq_zero_iff {α : Type u_1} [fintype α] :
fintype.card α = 0 ↔ is_empty α
source
theorem fintype.card_eq_zero {α : Type u_1} [fintype α] [is_empty α] :
fintype.card α = 0
source
theorem fintype.card_eq_one_iff_nonempty_unique {α : Type u_1} [fintype α] :
fintype.card α = 1 ↔ nonempty (unique α)
source
def fintype.card_eq_zero_equiv_equiv_empty {α : Type u_1} [fintype α] :
fintype.card α = 0 ≃ (α ≃ empty)

A fintype with cardinality zero is equivalent to empty.

Equations
source
theorem fintype.card_pos_iff {α : Type u_1} [fintype α] :
0 < fintype.card α ↔ nonempty α
source
theorem fintype.card_pos {α : Type u_1} [fintype α] [h : nonempty α] :
0 < fintype.card α
source
theorem fintype.card_ne_zero {α : Type u_1} [fintype α] [nonempty α] :
fintype.card α ≠ 0
source
theorem fintype.card_le_one_iff {α : Type u_1} [fintype α] :
fintype.card α ≤ 1 ↔ ∀ (a b : α), a = b
source
theorem fintype.card_le_one_iff_subsingleton {α : Type u_1} [fintype α] :
fintype.card α ≤ 1 ↔ subsingleton α
source
theorem fintype.one_lt_card_iff_nontrivial {α : Type u_1} [fintype α] :
1 < fintype.card α ↔ nontrivial α
source
theorem fintype.exists_ne_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < fintype.card α) (a : α) :
∃ (b : α), b ≠ a
source
theorem fintype.exists_pair_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < fintype.card α) :
∃ (a b : α), a ≠ b
source
theorem fintype.card_eq_one_of_forall_eq {α : Type u_1} [fintype α] {i : α} (h : ∀ (j : α), j = i) :
fintype.card α = 1
source
theorem fintype.one_lt_card {α : Type u_1} [fintype α] [h : nontrivial α] :
1 < fintype.card α
source
theorem fintype.one_lt_card_iff {α : Type u_1} [fintype α] :
1 < fintype.card α ↔ ∃ (a b : α), a ≠ b
source
theorem fintype.two_lt_card_iff {α : Type u_1} [fintype α] :
2 < fintype.card α ↔ ∃ (a b c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
source
theorem fintype.card_of_bijective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} (hf : function.bijective f) :
fintype.card α = fintype.card β
source
theorem finite.injective_iff_surjective {α : Type u_1} [finite α] {f : α → α} :
function.injective f ↔ function.surjective f
source
theorem finite.injective_iff_bijective {α : Type u_1} [finite α] {f : α → α} :
function.injective f ↔ function.bijective f
source
theorem finite.surjective_iff_bijective {α : Type u_1} [finite α] {f : α → α} :
function.surjective f ↔ function.bijective f
source
theorem finite.injective_iff_surjective_of_equiv {α : Type u_1} {β : Type u_2} [finite α] {f : α → β} (e : α ≃ β) :
function.injective f ↔ function.surjective f
source
theorem function.injective.bijective_of_finite {α : Type u_1} [finite α] {f : α → α} :
function.injective f → function.bijective f

Alias of the forward direction of finite.injective_iff_bijective.

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

Alias of the forward direction of finite.surjective_iff_bijective.

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

Alias of the forward direction of finite.injective_iff_surjective_of_equiv.

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

Alias of the reverse direction of finite.injective_iff_surjective_of_equiv.

source
theorem fintype.bijective_iff_injective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :
function.bijective f ↔ function.injective f ∧ fintype.card α = fintype.card β
source
theorem fintype.bijective_iff_surjective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :
function.bijective f ↔ function.surjective f ∧ fintype.card α = fintype.card β
source
theorem function.left_inverse.right_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} {g : β → α} (hfg : function.left_inverse f g) (hcard : fintype.card α ≤ fintype.card β) :
function.right_inverse f g
source
theorem function.right_inverse.left_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} {g : β → α} (hfg : function.right_inverse f g) (hcard : fintype.card β ≤ fintype.card α) :
function.left_inverse f g
source
def equiv.of_left_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : fintype.card β ≤ fintype.card α) (f : α → β) (g : β → α) (h : function.left_inverse g f) :
α ≃ β

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

Equations
source
@[simp]
theorem equiv.of_left_inverse_of_card_le_symm_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : fintype.card β ≤ fintype.card α) (f : α → β) (g : β → α) (h : function.left_inverse g f) (ᾰ : β) :
⇑((equiv.of_left_inverse_of_card_le hβα f g h).symm) ᾰ = g ᾰ
source
@[simp]
theorem equiv.of_left_inverse_of_card_le_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : fintype.card β ≤ fintype.card α) (f : α → β) (g : β → α) (h : function.left_inverse g f) (ᾰ : α) :
⇑(equiv.of_left_inverse_of_card_le hβα f g h) ᾰ = f ᾰ
source
def equiv.of_right_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : fintype.card α ≤ fintype.card β) (f : α → β) (g : β → α) (h : function.right_inverse g f) :
α ≃ β

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

Equations
source
@[simp]
theorem equiv.of_right_inverse_of_card_le_symm_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : fintype.card α ≤ fintype.card β) (f : α → β) (g : β → α) (h : function.right_inverse g f) (ᾰ : β) :
⇑((equiv.of_right_inverse_of_card_le hαβ f g h).symm) ᾰ = g ᾰ
source
@[simp]
theorem equiv.of_right_inverse_of_card_le_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : fintype.card α ≤ fintype.card β) (f : α → β) (g : β → α) (h : function.right_inverse g f) (ᾰ : α) :
⇑(equiv.of_right_inverse_of_card_le hαβ f g h) ᾰ = f ᾰ
source
@[simp]
theorem fintype.card_coe {α : Type u_1} (s : finset α) [fintype ↥s] :
fintype.card ↥s = s.card
source
noncomputable def finset.equiv_fin {α : Type u_1} (s : finset α) :
↥s ≃ fin s.card

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

Equations
source
noncomputable def finset.equiv_fin_of_card_eq {α : Type u_1} {s : finset α} {n : ℕ} (h : s.card = n) :
↥s ≃ fin n

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

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

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

Equations
source
@[simp]
theorem fintype.card_Prop  :
fintype.card Prop = 2
source
theorem set_fintype_card_le_univ {α : Type u_1} [fintype α] (s : set α) [fintype ↥s] :
fintype.card ↥s ≤ fintype.card α
source
theorem set_fintype_card_eq_univ_iff {α : Type u_1} [fintype α] (s : set α) [fintype ↥s] :
fintype.card ↥s = fintype.card α ↔ s = set.univ
source
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
source
@[simp]
theorem function.embedding.equiv_of_fintype_self_embedding_to_embedding {α : Type u_1} [finite α] (e : α ↪ α) :
e.equiv_of_fintype_self_embedding.to_embedding = e
source
@[simp]
theorem function.embedding.is_empty_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : fintype.card β < fintype.card α) :
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.

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

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

Equations
source
theorem function.embedding.nonempty_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : fintype.card α ≤ fintype.card β) :
nonempty (α ↪ β)
source
theorem function.embedding.nonempty_iff_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
nonempty (α ↪ β) ↔ fintype.card α ≤ fintype.card β
source
theorem function.embedding.exists_of_card_le_finset {α : Type u_1} {β : Type u_2} [fintype α] {s : finset β} (h : fintype.card α ≤ s.card) :
∃ (f : α ↪ β), set.range ⇑f ⊆ ↑s
source
@[simp]
theorem finset.univ_map_embedding {α : Type u_1} [fintype α] (e : α ↪ α) :
finset.map e finset.univ = finset.univ
source
theorem fintype.card_lt_of_surjective_not_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.surjective f) (h' : ¬function.injective f) :
fintype.card β < fintype.card α
source
theorem fintype.card_subtype_le {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
fintype.card {x // p x} ≤ fintype.card α
source
theorem fintype.card_subtype_lt {α : Type u_1} [fintype α] {p : α → Prop} [decidable_pred p] {x : α} (hx : ¬p x) :
fintype.card {x // p x} < fintype.card α
source
theorem fintype.card_subtype {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
fintype.card {x // p x} = (finset.filter p finset.univ).card
source
@[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 α - fintype.card {x // p x}
source
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}
source
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.

source
theorem fintype.card_quotient_le {α : Type u_1} [fintype α] (s : setoid α) [decidable_rel has_equiv.equiv] :
fintype.card (quotient s) ≤ fintype.card α
source
theorem fintype.card_quotient_lt {α : Type u_1} [fintype α] {s : setoid α} [decidable_rel has_equiv.equiv] {x y : α} (h1 : x ≠ y) (h2 : x ≈ y) :
fintype.card (quotient s) < fintype.card α
source
theorem univ_eq_singleton_of_card_one {α : Type u_1} [fintype α] (x : α) (h : fintype.card α = 1) :
finset.univ = {x}
source
theorem finite.well_founded_of_trans_of_irrefl {α : Type u_1} [finite α] (r : α → α → Prop) [is_trans α r] [is_irrefl α r] :
well_founded r
source
@[protected, instance]
def finite.finite.to_well_founded_lt {α : Type u_1} [finite α] [preorder α] :
well_founded_lt α
source
@[protected, instance]
def finite.finite.to_well_founded_gt {α : Type u_1} [finite α] [preorder α] :
well_founded_gt α
source
@[protected, instance]
def finite.linear_order.is_well_order_lt {α : Type u_1} [finite α] [linear_order α] :
is_well_order α has_lt.lt
source
@[protected, instance]
def finite.linear_order.is_well_order_gt {α : Type u_1} [finite α] [linear_order α] :
is_well_order α gt
source
@[protected, nolint]
theorem fintype.false {α : Type u_1} [infinite α] (h : fintype α) :
false
source
@[simp]
theorem is_empty_fintype {α : Type u_1} :
is_empty (fintype α) ↔ infinite α
source
noncomputable def fintype_of_not_infinite {α : Type u_1} (h : ¬infinite α) :
fintype α

A non-infinite type is a fintype.

Equations
source
noncomputable def fintype_or_infinite (α : Type u_1) :
psum (fintype α) (infinite α)

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

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

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

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

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

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

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

Embedding of ℕ into an infinite type.

Equations
source
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.

source
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.

source
noncomputable def fintype_of_finset_card_le {ι : Type u_1} (n : ℕ) (w : ∀ (s : finset ι), s.card ≤ n) :
fintype ι

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

Equations
source
theorem not_injective_infinite_finite {α : Sort u_1} {β : Sort u_2} [infinite α] [finite β] (f : α → β) :
¬function.injective f
source
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.

source
@[protected, instance]
def function.embedding.is_empty {α : Sort u_1} {β : Sort u_2} [infinite α] [finite β] :
is_empty (α ↪ β)
source
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

source
theorem not_surjective_finite_infinite {α : Sort u_1} {β : Sort u_2} [finite α] [infinite β] (f : α → β) :
¬function.surjective f
source
def trunc_of_card_pos {α : Type u_1} [fintype α] (h : 0 < fintype.card α) :
trunc α

A fintype with positive cardinality constructively contains an element.

Equations
source
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 : subsingleton α], P α) (hstep : ∀ (α : Type u_1) [_inst_5 : fintype α] [_inst_6 : nontrivial α], (∀ (β : Type u_1) [_inst_7 : fintype β], fintype.card β < fintype.card α → 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.

source
meta def tactic.positivity_finset_card  :
expr → tactic tactic.positivity.strictness

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