mathlib documentation

data.fintype.basic

Finite types #

This file defines a typeclass to state that a type is finite.

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.

Instances #

Among others, we provide fintype instances for

and infinite instances for

along with some machinery

source
@[class]
structure fintype (α : Type u_4) :
Type u_4

fintype α means that α is finite, i.e. there are only finitely many distinct elements of type α. The evidence of this is a finset elems (a list up to permutation without duplicates), together with a proof that everything of type α is in the list.

Instances
source
def finset.univ {α : Type u_1} [fintype α] :
finset α

univ is the universal finite set of type finset α implied from the assumption fintype α.

Equations
source
@[simp]
theorem finset.mem_univ {α : Type u_1} [fintype α] (x : α) :
x ∈ finset.univ
source
@[simp]
theorem finset.mem_univ_val {α : Type u_1} [fintype α] (x : α) :
x ∈ finset.univ.val
source
theorem finset.eq_univ_iff_forall {α : Type u_1} [fintype α] {s : finset α} :
s = finset.univ ↔ ∀ (x : α), x ∈ s
source
@[simp]
theorem finset.coe_univ {α : Type u_1} [fintype α] :
↑finset.univ = set.univ
source
theorem finset.univ_nonempty_iff {α : Type u_1} [fintype α] :
finset.univ.nonempty ↔ nonempty α
source
theorem finset.univ_nonempty {α : Type u_1} [fintype α] [nonempty α] :
finset.univ.nonempty
source
theorem finset.univ_eq_empty_iff {α : Type u_1} [fintype α] :
finset.univ = ∅ ↔ is_empty α
source
@[simp]
theorem finset.univ_eq_empty {α : Type u_1} [fintype α] [is_empty α] :
finset.univ = ∅
source
@[simp]
theorem finset.univ_unique {α : Type u_1} [fintype α] [unique α] :
finset.univ = {default}
source
@[simp]
theorem finset.subset_univ {α : Type u_1} [fintype α] (s : finset α) :
s ⊆ finset.univ
source
@[protected, instance]
def finset.order_top {α : Type u_1} [fintype α] :
order_top (finset α)
Equations
source
@[protected, instance]
def finset.boolean_algebra {α : Type u_1} [fintype α] [decidable_eq α] :
boolean_algebra (finset α)
Equations
source
theorem finset.compl_eq_univ_sdiff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
sᶜ = finset.univ \ s
source
@[simp]
theorem finset.mem_compl {α : Type u_1} [fintype α] [decidable_eq α] {s : finset α} {a : α} :
a ∈ sᶜ ↔ a ∉ s
source
theorem finset.not_mem_compl {α : Type u_1} [fintype α] [decidable_eq α] {s : finset α} {a : α} :
a ∉ sᶜ ↔ a ∈ s
source
@[simp, norm_cast]
theorem finset.coe_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
↑sᶜ = (↑s)ᶜ
source
@[simp]
theorem finset.compl_empty {α : Type u_1} [fintype α] [decidable_eq α] :
∅ᶜ = finset.univ
source
@[simp]
theorem finset.union_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
s ∪ sᶜ = finset.univ
source
@[simp]
theorem finset.inter_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
s ∩ sᶜ = ∅
source
@[simp]
theorem finset.compl_union {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :
(s ∪ t)ᶜ = sᶜ ∩ tᶜ
source
@[simp]
theorem finset.compl_inter {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :
(s ∩ t)ᶜ = sᶜ ∪ tᶜ
source
@[simp]
theorem finset.compl_erase {α : Type u_1} [fintype α] [decidable_eq α] {s : finset α} {a : α} :
(s.erase a)ᶜ = insert a sᶜ
source
@[simp]
theorem finset.compl_insert {α : Type u_1} [fintype α] [decidable_eq α] {s : finset α} {a : α} :
(insert a s)ᶜ = sᶜ.erase a
source
@[simp]
theorem finset.insert_compl_self {α : Type u_1} [fintype α] [decidable_eq α] (x : α) :
insert x {x}ᶜ = finset.univ
source
@[simp]
theorem finset.compl_filter {α : Type u_1} [fintype α] [decidable_eq α] (p : α → Prop) [decidable_pred p] [Π (x : α), decidable (¬p x)] :
(finset.filter p finset.univ)ᶜ = finset.filter (λ (x : α), ¬p x) finset.univ
source
theorem finset.compl_ne_univ_iff_nonempty {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
sᶜ ≠ finset.univ ↔ s.nonempty
source
theorem finset.compl_singleton {α : Type u_1} [fintype α] [decidable_eq α] (a : α) :
{a}ᶜ = finset.univ.erase a
source
theorem finset.insert_inj_on' {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
set.inj_on (λ (a : α), insert a s) ↑sᶜ
source
@[simp]
theorem finset.univ_inter {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
finset.univ ∩ s = s
source
@[simp]
theorem finset.inter_univ {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
s ∩ finset.univ = s
source
@[simp]
theorem finset.piecewise_univ {α : Type u_1} [fintype α] [Π (i : α), decidable (i ∈ finset.univ)] {δ : α → Sort u_2} (f g : Π (i : α), δ i) :
finset.univ.piecewise f g = f
source
theorem finset.piecewise_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) [Π (i : α), decidable (i ∈ s)] [Π (i : α), decidable (i ∈ sᶜ)] {δ : α → Sort u_2} (f g : Π (i : α), δ i) :
sᶜ.piecewise f g = s.piecewise g f
source
@[simp]
theorem finset.piecewise_erase_univ {α : Type u_1} [fintype α] {δ : α → Sort u_2} [decidable_eq α] (a : α) (f g : Π (a : α), δ a) :
(finset.univ.erase a).piecewise f g = function.update f a (g a)
source
theorem finset.univ_map_equiv_to_embedding {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (e : α ≃ β) :
finset.map e.to_embedding finset.univ = finset.univ
source
@[simp]
theorem finset.univ_filter_exists {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) [fintype β] [decidable_pred (λ (y : β), ∃ (x : α), f x = y)] [decidable_eq β] :
finset.filter (λ (y : β), ∃ (x : α), f x = y) finset.univ = finset.image f finset.univ
source
theorem finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) [fintype β] [decidable_pred (λ (y : β), y ∈ set.range f)] [decidable_eq β] :
finset.filter (λ (y : β), y ∈ set.range f) finset.univ = finset.image f finset.univ

Note this is a special case of (finset.image_preimage f univ _).symm.

source
theorem finset.coe_filter_univ {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
↑(finset.filter p finset.univ) = {x : α | p x}
source
theorem finset.sup_univ_eq_supr {α : Type u_1} {β : Type u_2} [fintype α] [complete_lattice β] (f : α → β) :
finset.univ.sup f = supr f

A special case of finset.sup_eq_supr that omits the useless x ∈ univ binder.

source
theorem finset.inf_univ_eq_infi {α : Type u_1} {β : Type u_2} [fintype α] [complete_lattice β] (f : α → β) :
finset.univ.inf f = infi f

A special case of finset.inf_eq_infi that omits the useless x ∈ univ binder.

source
@[simp]
theorem finset.fold_inf_univ {α : Type u_1} [fintype α] [semilattice_inf α] [order_bot α] (a : α) :
finset.fold has_inf.inf a (λ (x : α), x) finset.univ = ⊥
source
@[simp]
theorem finset.fold_sup_univ {α : Type u_1} [fintype α] [semilattice_sup α] [order_top α] (a : α) :
finset.fold has_sup.sup a (λ (x : α), x) finset.univ = ⊤
source
@[protected, instance]
def fintype.decidable_pi_fintype {α : Type u_1} {β : α → Type u_2} [Π (a : α), decidable_eq (β a)] [fintype α] :
decidable_eq (Π (a : α), β a)
Equations
source
@[protected, instance]
def fintype.decidable_forall_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :
decidable (∀ (a : α), p a)
Equations
source
@[protected, instance]
def fintype.decidable_exists_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :
decidable (∃ (a : α), p a)
Equations
source
@[protected, instance]
def fintype.decidable_mem_range_fintype {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α → β) :
decidable_pred (λ (_x : β), _x ∈ set.range f)
Equations
source
@[protected, instance]
def fintype.decidable_eq_equiv_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :
decidable_eq (α ≃ β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_embedding_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :
decidable_eq (α ↪ β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_one_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_one α] [has_one β] :
decidable_eq (one_hom α β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_zero_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_zero α] [has_zero β] :
decidable_eq (zero_hom α β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_mul_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_mul α] [has_mul β] :
decidable_eq (α →ₙ* β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_add_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_add α] [has_add β] :
decidable_eq (add_hom α β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_add_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [add_zero_class α] [add_zero_class β] :
decidable_eq (α →+ β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [mul_one_class α] [mul_one_class β] :
decidable_eq (α →* β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_monoid_with_zero_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [mul_zero_one_class α] [mul_zero_one_class β] :
decidable_eq (α →*₀ β)
Equations
source
@[protected, instance]
def fintype.decidable_eq_ring_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [semiring α] [semiring β] :
decidable_eq (α →+* β)
Equations
source
@[protected, instance]
def fintype.decidable_injective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] :
decidable_pred function.injective
Equations
source
@[protected, instance]
def fintype.decidable_surjective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [fintype β] :
decidable_pred function.surjective
Equations
source
@[protected, instance]
def fintype.decidable_bijective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
decidable_pred function.bijective
Equations
source
@[protected, instance]
def fintype.decidable_right_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] (f : α → β) (g : β → α) :
decidable (function.right_inverse f g)
Equations
source
@[protected, instance]
def fintype.decidable_left_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype β] (f : α → β) (g : β → α) :
decidable (function.left_inverse f g)
Equations
source
theorem fintype.exists_max {α : Type u_1} [fintype α] [nonempty α] {β : Type u_2} [linear_order β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀
source
theorem fintype.exists_min {α : Type u_1} [fintype α] [nonempty α] {β : Type u_2} [linear_order β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x₀ ≤ f x
source
def fintype.of_multiset {α : Type u_1} [decidable_eq α] (s : multiset α) (H : ∀ (x : α), x ∈ s) :
fintype α

Construct a proof of fintype α from a universal multiset

Equations
source
def fintype.of_list {α : Type u_1} [decidable_eq α] (l : list α) (H : ∀ (x : α), x ∈ l) :
fintype α

Construct a proof of fintype α from a universal list

Equations
source
theorem fintype.exists_univ_list (α : Type u_1) [fintype α] :
∃ (l : list α), l.nodup ∧ ∀ (x : α), x ∈ l
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
@[protected, instance]
def fintype.subsingleton (α : Type u_1) :
subsingleton (fintype α)
source
@[protected]
def fintype.subtype {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ p x) :
fintype {x // p x}

Given a predicate that can be represented by a finset, the subtype associated to the predicate is a fintype.

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
def fintype.of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :
fintype ↥p

Construct a fintype from a finset with the same elements.

Equations
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
def fintype.of_bijective {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) (H : function.bijective f) :
fintype β

If f : α → β is a bijection and α is a fintype, then β is also a fintype.

Equations
source
def fintype.of_surjective {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] (f : α → β) (H : function.surjective f) :
fintype β

If f : α → β is a surjection and α is a fintype, then β is also a fintype.

Equations
source
def function.injective.inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) :
↥(set.range f) → α

The inverse of an hf : injective function f : α → β, of the type ↥(set.range f) → α. This is the computable version of function.inv_fun that requires fintype α and decidable_eq β, or the function version of applying (equiv.of_injective f hf).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = fintype.card α.

Equations
source
theorem function.injective.left_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) (b : ↥(set.range f)) :
f (hf.inv_of_mem_range b) = ↑b
source
@[simp]
theorem function.injective.right_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) (a : α) :
hf.inv_of_mem_range ⟨f a, _⟩ = a
source
theorem function.injective.inv_fun_restrict {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) [nonempty α] :
(set.range f).restrict (function.inv_fun f) = hf.inv_of_mem_range
source
theorem function.injective.inv_of_mem_range_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) :
function.surjective hf.inv_of_mem_range
source
def function.embedding.inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (b : ↥(set.range ⇑f)) :
α

The inverse of an embedding f : α ↪ β, of the type ↥(set.range f) → α. This is the computable version of function.inv_fun that requires fintype α and decidable_eq β, or the function version of applying (equiv.of_injective f f.injective).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = fintype.card α.

Equations
source
@[simp]
theorem function.embedding.left_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (b : ↥(set.range ⇑f)) :
⇑f (f.inv_of_mem_range b) = ↑b
source
@[simp]
theorem function.embedding.right_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (a : α) :
f.inv_of_mem_range ⟨⇑f a, _⟩ = a
source
theorem function.embedding.inv_fun_restrict {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) [nonempty α] :
(set.range ⇑f).restrict (function.inv_fun ⇑f) = f.inv_of_mem_range
source
theorem function.embedding.inv_of_mem_range_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) :
function.surjective f.inv_of_mem_range
source
noncomputable def fintype.of_injective {α : Type u_1} {β : Type u_2} [fintype β] (f : α → β) (H : function.injective f) :
fintype α

Given an injective function to a fintype, the domain is also a fintype. This is noncomputable because injectivity alone cannot be used to construct preimages.

Equations
source
def fintype.of_equiv {β : Type u_2} (α : Type u_1) [fintype α] (f : α ≃ β) :
fintype β

If f : α ≃ β and α is a fintype, then β is also a fintype.

Equations
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
def fintype.of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :
fintype α

Any subsingleton type with a witness is a fintype (with one term).

Equations
source
@[simp]
theorem fintype.univ_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :
finset.univ = {a}
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
@[protected, instance]
def fintype.of_is_empty {α : Type u_1} [is_empty α] :
fintype α
Equations
source
@[simp, nolint]
theorem fintype.univ_of_is_empty {α : Type u_1} [is_empty α] :
finset.univ = ∅

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

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
@[protected, instance]
noncomputable def fintype.of_subsingleton' (α : Type u_1) [subsingleton α] :
fintype α

Any subsingleton type is (noncomputably) a fintype (with zero or one term).

Equations
source
def set.to_finset {α : Type u_1} (s : set α) [fintype ↥s] :
finset α

Construct a finset enumerating a set s, given a fintype instance.

Equations
source
theorem set.to_finset_congr {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] (h : s = t) :
s.to_finset = t.to_finset
source
@[simp]
theorem set.mem_to_finset {α : Type u_1} {s : set α} [fintype ↥s] {a : α} :
a ∈ s.to_finset ↔ a ∈ s
source
@[simp]
theorem set.mem_to_finset_val {α : Type u_1} {s : set α} [fintype ↥s] {a : α} :
a ∈ s.to_finset.val ↔ a ∈ s
source
@[simp]
theorem set.to_finset_card {α : Type u_1} (s : set α) [fintype ↥s] :
s.to_finset.card = fintype.card ↥s
source
@[simp]
theorem set.coe_to_finset {α : Type u_1} (s : set α) [fintype ↥s] :
↑(s.to_finset) = s
source
@[simp]
theorem set.to_finset_inj {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
s.to_finset = t.to_finset ↔ s = t
source
@[simp]
theorem set.to_finset_mono {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
s.to_finset ⊆ t.to_finset ↔ s ⊆ t
source
@[simp]
theorem set.to_finset_strict_mono {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
s.to_finset ⊂ t.to_finset ↔ s ⊂ t
source
@[simp]
theorem set.to_finset_disjoint_iff {α : Type u_1} [decidable_eq α] {s t : set α} [fintype ↥s] [fintype ↥t] :
disjoint s.to_finset t.to_finset ↔ disjoint s t
source
theorem set.to_finset_compl {α : Type u_1} [decidable_eq α] [fintype α] (s : set α) [fintype ↥s] [fintype ↥sᶜ] :
sᶜ.to_finset = s.to_finsetᶜ
source
theorem set.filter_mem_univ_eq_to_finset {α : Type u_1} [fintype α] (s : set α) [fintype ↥s] [decidable_pred (λ (_x : α), _x ∈ s)] :
finset.filter (λ (_x : α), _x ∈ s) finset.univ = s.to_finset
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
@[protected, instance]
def fin.fintype (n : ℕ) :
fintype (fin n)
Equations
source
theorem fin.univ_def (n : ℕ) :
finset.univ = finset.fin_range n
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 fin.image_succ_above_univ {n : ℕ} (i : fin (n + 1)) :
finset.image ⇑(i.succ_above) finset.univ = {i}ᶜ
source
@[simp]
theorem fin.image_succ_univ (n : ℕ) :
finset.image fin.succ finset.univ = {0}ᶜ
source
@[simp]
theorem fin.image_cast_succ (n : ℕ) :
finset.image ⇑fin.cast_succ finset.univ = {fin.last n}ᶜ
source
theorem fin.univ_succ (n : ℕ) :
finset.univ = insert 0 (finset.image fin.succ finset.univ)

Embed fin n into fin (n + 1) by prepending zero to the univ

source
theorem fin.univ_cast_succ (n : ℕ) :
finset.univ = insert (fin.last n) (finset.image ⇑fin.cast_succ finset.univ)

Embed fin n into fin (n + 1) by appending a new fin.last n to the univ

source
theorem fin.univ_succ_above (n : ℕ) (p : fin (n + 1)) :
finset.univ = insert p (finset.image ⇑(p.succ_above) finset.univ)

Embed fin n into fin (n + 1) by inserting around a specified pivot p : fin (n + 1) into the univ

source
@[instance]
def unique.fintype {α : Type u_1} [unique α] :
fintype α
Equations
source
@[protected, instance]
def fintype.subtype_eq {α : Type u_1} (y : α) :
fintype {x // x = y}

Short-circuit instance to decrease search for unique.fintype, since that relies on a subsingleton elimination for unique.

Equations
source
@[protected, instance]
def fintype.subtype_eq' {α : Type u_1} (y : α) :
fintype {x // y = x}

Short-circuit instance to decrease search for unique.fintype, since that relies on a subsingleton elimination for unique.

Equations
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.univ_empty  :
finset.univ = ∅
source
@[simp]
theorem fintype.card_empty  :
fintype.card empty = 0
source
@[simp]
theorem fintype.univ_pempty  :
finset.univ = ∅
source
@[simp]
theorem fintype.card_pempty  :
fintype.card pempty = 0
source
@[protected, instance]
def unit.fintype  :
fintype unit
Equations
source
theorem fintype.univ_unit  :
finset.univ = {()}
source
theorem fintype.card_unit  :
fintype.card unit = 1
source
@[protected, instance]
def punit.fintype  :
fintype punit
Equations
source
@[simp]
theorem fintype.univ_punit  :
finset.univ = {punit.star}
source
@[simp]
theorem fintype.card_punit  :
fintype.card punit = 1
source
@[protected, instance]
def bool.fintype  :
fintype bool
Equations
source
@[simp]
theorem fintype.univ_bool  :
finset.univ = {tt, ff}
source
@[protected, instance]
def units_int.fintype  :
fintype ℤˣ
Equations
source
@[simp]
theorem units_int.univ  :
finset.univ = {1, -1}
source
@[protected, instance]
def additive.fintype {α : Type u_1} [fintype α] :
fintype (additive α)
Equations
source
@[protected, instance]
def multiplicative.fintype {α : Type u_1} [fintype α] :
fintype (multiplicative α)
Equations
source
@[simp]
theorem fintype.card_units_int  :
fintype.card ℤˣ = 2
source
@[simp]
theorem fintype.card_bool  :
fintype.card bool = 2
source
@[protected, instance]
def option.fintype {α : Type u_1} [fintype α] :
fintype (option α)
Equations
source
theorem univ_option (α : Type u_1) [fintype α] :
finset.univ = ⇑finset.insert_none finset.univ
source
@[simp]
theorem fintype.card_option {α : Type u_1} [fintype α] :
fintype.card (option α) = fintype.card α + 1
source
def fintype_of_option {α : Type u_1} [fintype (option α)] :
fintype α

If option α is a fintype then so is α

Equations
source
def fintype_of_option_equiv {α : Type u_1} {β : Type u_2} [fintype α] (f : option α ≃ β) :
fintype β

A type is a fintype if its successor (using option) is a fintype.

Equations
source
@[protected, instance]
def sigma.fintype {α : Type u_1} (β : α → Type u_2) [fintype α] [Π (a : α), fintype (β a)] :
fintype (sigma β)
Equations
source
@[simp]
theorem finset.univ_sigma_univ {α : Type u_1} {β : α → Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
finset.univ.sigma (λ (a : α), finset.univ) = finset.univ
source
@[protected, instance]
def prod.fintype (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
fintype (α × β)
Equations
source
@[simp]
theorem finset.univ_product_univ {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
finset.univ.product finset.univ = finset.univ
source
@[simp]
theorem fintype.card_prod (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
fintype.card (α × β) = (fintype.card α) * fintype.card β
source
def fintype.prod_left {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype (α × β)] [nonempty β] :
fintype α

Given that α × β is a fintype, α is also a fintype.

Equations
source
def fintype.prod_right {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype (α × β)] [nonempty α] :
fintype β

Given that α × β is a fintype, β is also a fintype.

Equations
source
@[protected, instance]
def ulift.fintype (α : Type u_1) [fintype α] :
fintype (ulift α)
Equations
source
@[simp]
theorem fintype.card_ulift (α : Type u_1) [fintype α] :
fintype.card (ulift α) = fintype.card α
source
@[protected, instance]
def plift.fintype (α : Type u_1) [fintype α] :
fintype (plift α)
Equations
source
@[simp]
theorem fintype.card_plift (α : Type u_1) [fintype α] :
fintype.card (plift α) = fintype.card α
source
@[protected, instance]
def order_dual.fintype (α : Type u_1) [fintype α] :
fintype (order_dual α)
Equations
source
@[simp]
theorem fintype.card_order_dual (α : Type u_1) [fintype α] :
fintype.card (order_dual α) = fintype.card α
source
@[protected, instance]
def lex.fintype (α : Type u_1) [fintype α] :
fintype (lex α)
Equations
source
@[simp]
theorem fintype.card_lex (α : Type u_1) [fintype α] :
fintype.card (lex α) = fintype.card α
source
theorem univ_sum_type {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [fintype (α ⊕ β)] [decidable_eq (α ⊕ β)] :
finset.univ = finset.map function.embedding.inl finset.univ ∪ finset.map function.embedding.inr finset.univ
source
@[protected, instance]
def sum.fintype (α : Type u) (β : Type v) [fintype α] [fintype β] :
fintype (α ⊕ β)
Equations
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
source
@[simp]
theorem fintype.card_sum {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
fintype.card (α ⊕ β) = fintype.card α + fintype.card β
source
def fintype_of_fintype_ne {α : Type u_1} (a : α) [decidable_pred (λ (_x : α), _x = a)] (h : fintype {b // b ≠ a}) :
fintype α

If the subtype of all-but-one elements is a fintype then the type itself is a fintype.

Equations

fintype (s : finset α) #

source
@[protected, instance]
def finset.fintype_coe_sort {α : Type u} (s : finset α) :
fintype ↥s
Equations
source
@[simp]
theorem finset.univ_eq_attach {α : Type u} (s : finset α) :
finset.univ = s.attach
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.injective_iff_surjective {α : Type u_1} [fintype α] {f : α → α} :
function.injective f ↔ function.surjective f
source
theorem fintype.injective_iff_bijective {α : Type u_1} [fintype α] {f : α → α} :
function.injective f ↔ function.bijective f
source
theorem fintype.surjective_iff_bijective {α : Type u_1} [fintype α] {f : α → α} :
function.surjective f ↔ function.bijective f
source
theorem fintype.injective_iff_surjective_of_equiv {α : Type u_1} [fintype α] {β : Type u_2} {f : α → β} (e : α ≃ β) :
function.injective f ↔ function.surjective f
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 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 fintype.right_inverse_of_left_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 fintype.left_inverse_of_right_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
theorem fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} :
↑(finset.image f finset.univ) = set.range f
source
@[protected, instance]
def list.subtype.fintype {α : Type u_1} [decidable_eq α] (l : list α) :
fintype {x // x ∈ l}
Equations
source
@[protected, instance]
def multiset.subtype.fintype {α : Type u_1} [decidable_eq α] (s : multiset α) :
fintype {x // x ∈ s}
Equations
source
@[protected, instance]
def finset.subtype.fintype {α : Type u_1} (s : finset α) :
fintype {x // x ∈ s}
Equations
source
@[protected, instance]
def finset_coe.fintype {α : Type u_1} (s : finset α) :
fintype ↥↑s
Equations
source
@[simp]
theorem fintype.card_coe {α : Type u_1} (s : finset α) [fintype ↥s] :
fintype.card ↥s = s.card
source
theorem finset.attach_eq_univ {α : Type u_1} {s : finset α} :
s.attach = finset.univ
source
@[protected, instance]
def plift.fintype_Prop (p : Prop) [decidable p] :
fintype (plift p)
Equations
source
@[protected, instance]
def Prop.fintype  :
fintype Prop
Equations
source
@[simp]
theorem fintype.card_Prop  :
fintype.card Prop = 2
source
@[protected, instance]
def subtype.fintype {α : Type u_1} (p : α → Prop) [decidable_pred p] [fintype α] :
fintype {x // p x}
Equations
source
@[simp]
theorem set.to_finset_univ {α : Type u_1} [fintype ↥set.univ] [fintype α] :
set.univ.to_finset = finset.univ
source
@[simp]
theorem set.to_finset_eq_empty_iff {α : Type u_1} {s : set α} [fintype ↥s] :
s.to_finset = ∅ ↔ s = ∅
source
@[simp]
theorem set.to_finset_empty {α : Type u_1} :
∅.to_finset = ∅
source
@[simp]
theorem set.to_finset_range {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype β] (f : β → α) [fintype ↥(set.range f)] :
(set.range f).to_finset = finset.image f finset.univ
source
def set_fintype {α : Type u_1} [fintype α] (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] :
fintype ↥s

A set on a fintype, when coerced to a type, is a fintype.

Equations
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
@[simp]
theorem coe_units_equiv_prod_subtype_symm_apply (α : Type u_1) [monoid α] (p : {p // (p.fst) * p.snd = 1 ∧ (p.snd) * p.fst = 1}) :
↑(⇑((units_equiv_prod_subtype α).symm) p) = ↑p.fst
source
@[simp]
theorem units_equiv_prod_subtype_apply_coe (α : Type u_1) [monoid α] (u : αˣ) :
↑(⇑(units_equiv_prod_subtype α) u) = (↑u, ↑u⁻¹)
source
@[simp]
theorem coe_inv_units_equiv_prod_subtype_symm_apply (α : Type u_1) [monoid α] (p : {p // (p.fst) * p.snd = 1 ∧ (p.snd) * p.fst = 1}) :
↑(⇑((units_equiv_prod_subtype α).symm) p)⁻¹ = ↑p.snd
source
def units_equiv_prod_subtype (α : Type u_1) [monoid α] :
αˣ ≃ {p // (p.fst) * p.snd = 1 ∧ (p.snd) * p.fst = 1}

The αˣ type is equivalent to a subtype of α × α.

Equations
source
@[simp]
theorem units_equiv_ne_zero_apply_coe (α : Type u_1) [group_with_zero α] (a : αˣ) :
↑(⇑(units_equiv_ne_zero α) a) = ↑a
source
def units_equiv_ne_zero (α : Type u_1) [group_with_zero α] :
αˣ ≃ {a // a ≠ 0}

In a group_with_zero α, the unit group αˣ is equivalent to the subtype of nonzero elements.

Equations
source
@[simp]
theorem units_equiv_ne_zero_symm_apply (α : Type u_1) [group_with_zero α] (a : {a // a ≠ 0}) :
⇑((units_equiv_ne_zero α).symm) a = units.mk0 ↑a _
source
@[protected, instance]
def units.fintype {α : Type u_1} [monoid α] [fintype α] [decidable_eq α] :
fintype αˣ
Equations
source
theorem fintype.card_units {α : Type u_1} [group_with_zero α] [fintype α] [fintype αˣ] :
fintype.card αˣ = fintype.card α - 1
source
noncomputable def function.embedding.equiv_of_fintype_self_embedding {α : Type u_1} [fintype α] (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} [fintype α] (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.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
def fintype.pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (t : Π (a : α), finset (δ a)) :
finset (Π (a : α), δ a)

Given for all a : α a finset t a of δ a, then one can define the finset fintype.pi_finset t of all functions taking values in t a for all a. This is the analogue of finset.pi where the base finset is univ (but formally they are not the same, as there is an additional condition i ∈ finset.univ in the finset.pi definition).

Equations
source
@[simp]
theorem fintype.mem_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a} :
f ∈ fintype.pi_finset t ↔ ∀ (a : α), f a ∈ t a
source
@[simp]
theorem fintype.coe_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (t : Π (a : α), finset (δ a)) :
↑(fintype.pi_finset t) = set.univ.pi (λ (a : α), ↑(t a))
source
theorem fintype.pi_finset_subset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (t₁ t₂ : Π (a : α), finset (δ a)) (h : ∀ (a : α), t₁ a ⊆ t₂ a) :
fintype.pi_finset t₁ ⊆ fintype.pi_finset t₂
source
theorem fintype.pi_finset_disjoint_of_disjoint {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} [Π (a : α), decidable_eq (δ a)] (t₁ t₂ : Π (a : α), finset (δ a)) {a : α} (h : disjoint (t₁ a) (t₂ a)) :
disjoint (fintype.pi_finset t₁) (fintype.pi_finset t₂)

pi #

source
@[protected, instance]
def pi.fintype {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
fintype (Π (a : α), β a)

A dependent product of fintypes, indexed by a fintype, is a fintype.

Equations
source
@[simp]
theorem fintype.pi_finset_univ {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
fintype.pi_finset (λ (a : α), finset.univ) = finset.univ
source
@[protected, instance]
def d_array.fintype {n : ℕ} {α : fin n → Type u_1} [Π (n : fin n), fintype (α n)] :
fintype (d_array n α)
Equations
source
@[protected, instance]
def array.fintype {n : ℕ} {α : Type u_1} [fintype α] :
fintype (array n α)
Equations
source
@[protected, instance]
def vector.fintype {α : Type u_1} [fintype α] {n : ℕ} :
fintype (vector α n)
Equations
source
@[protected, instance]
def quotient.fintype {α : Type u_1} [fintype α] (s : setoid α) [decidable_rel has_equiv.equiv] :
fintype (quotient s)
Equations
source
@[protected, instance]
def finset.fintype {α : Type u_1} [fintype α] :
fintype (finset α)
Equations
source
@[protected, instance]
def function.embedding.fintype {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] :
fintype (α ↪ β)
Equations
source
@[protected, instance]
def sym.sym'.fintype {α : Type u_1} [decidable_eq α] [fintype α] {n : ℕ} :
fintype (sym.sym' α n)
Equations
source
@[protected, instance]
def sym.fintype {α : Type u_1} [decidable_eq α] [fintype α] {n : ℕ} :
fintype (sym α n)
Equations
source
@[simp]
theorem fintype.card_finset {α : Type u_1} [fintype α] :
fintype.card (finset α) = 2 ^ fintype.card α
source
theorem finset.mem_powerset_len_univ_iff {α : Type u_1} [fintype α] {s : finset α} {k : ℕ} :
s ∈ finset.powerset_len k finset.univ ↔ s.card = k
source
@[simp]
theorem finset.univ_filter_card_eq (α : Type u_1) [fintype α] (k : ℕ) :
finset.filter (λ (s : finset α), s.card = k) finset.univ = finset.powerset_len k finset.univ
source
@[simp]
theorem fintype.card_finset_len {α : Type u_1} [fintype α] (k : ℕ) :
fintype.card {s // s.card = k} = (fintype.card α).choose k
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
theorem fintype.card_subtype_or {α : Type u_1} (p q : α → Prop) [fintype {x // p x}] [fintype {x // q x}] [fintype {x // p x ∨ q x}] :
fintype.card {x // p x ∨ q x} ≤ fintype.card {x // p x} + fintype.card {x // q x}
source
theorem fintype.card_subtype_or_disjoint {α : Type u_1} (p q : α → Prop) (h : disjoint p q) [fintype {x // p x}] [fintype {x // q x}] [fintype {x // p x ∨ q x}] :
fintype.card {x // p x ∨ q x} = fintype.card {x // p x} + fintype.card {x // q x}
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
@[protected, instance]
def psigma.fintype {α : Type u_1} {β : α → Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def psigma.fintype_prop_left {α : Prop} {β : α → Type u_1} [decidable α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def psigma.fintype_prop_right {α : Type u_1} {β : α → Prop} [Π (a : α), decidable (β a)] [fintype α] :
fintype (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [Π (a : α), decidable (β a)] :
fintype (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def set.fintype {α : Type u_1} [fintype α] :
fintype (set α)
Equations
source
@[simp]
theorem fintype.card_set {α : Type u_1} [fintype α] :
fintype.card (set α) = 2 ^ fintype.card α
source
@[protected, instance]
def pfun_fintype (p : Prop) [decidable p] (α : p → Type u_1) [Π (hp : p), fintype (α hp)] :
fintype (Π (hp : p), α hp)
Equations
source
@[simp]
theorem finset.univ_pi_univ {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
finset.univ.pi (λ (a : α), finset.univ) = finset.univ
source
theorem mem_image_univ_iff_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} {b : β} :
b ∈ finset.image f finset.univ ↔ b ∈ set.range f
source
def quotient.fin_choice_aux {ι : Type u_1} [decidable_eq ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) :
(Π (i : ι), i ∈ l → quotient (S i)) → quotient pi_setoid

An auxiliary function for quotient.fin_choice. Given a collection of setoids indexed by a type ι, a (finite) list l of indices, and a function that for each i ∈ l gives a term of the corresponding quotient type, then there is a corresponding term in the quotient of the product of the setoids indexed by l.

Equations
source
theorem quotient.fin_choice_aux_eq {ι : Type u_1} [decidable_eq ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) (f : Π (i : ι), i ∈ l → α i) :
quotient.fin_choice_aux l (λ (i : ι) (h : i ∈ l), ⟦f i h⟧) = ⟦f⟧
source
def quotient.fin_choice {ι : Type u_1} [decidable_eq ι] [fintype ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (f : Π (i : ι), quotient (S i)) :
quotient pi_setoid

Given a collection of setoids indexed by a fintype ι and a function that for each i : ι gives a term of the corresponding quotient type, then there is corresponding term in the quotient of the product of the setoids.

Equations
source
theorem quotient.fin_choice_eq {ι : Type u_1} [decidable_eq ι] [fintype ι] {α : ι → Type u_2} [Π (i : ι), setoid (α i)] (f : Π (i : ι), α i) :
quotient.fin_choice (λ (i : ι), ⟦f i⟧) = ⟦f⟧
source
def perms_of_list {α : Type u_1} [decidable_eq α] :
list α → list (equiv.perm α)

Given a list, produce a list of all permutations of its elements.

Equations
source
theorem length_perms_of_list {α : Type u_1} [decidable_eq α] (l : list α) :
(perms_of_list l).length = (l.length)!
source
theorem mem_perms_of_list_of_mem {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} (h : ∀ (x : α), ⇑f x ≠ x → x ∈ l) :
f ∈ perms_of_list l
source
theorem mem_of_mem_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
f ∈ perms_of_list l → ∀ {x : α}, ⇑f x ≠ x → x ∈ l
source
theorem mem_perms_of_list_iff {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
f ∈ perms_of_list l ↔ ∀ {x : α}, ⇑f x ≠ x → x ∈ l
source
theorem nodup_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) :
(perms_of_list l).nodup
source
def perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
finset (equiv.perm α)

Given a finset, produce the finset of all permutations of its elements.

Equations
source
theorem mem_perms_of_finset_iff {α : Type u_1} [decidable_eq α] {s : finset α} {f : equiv.perm α} :
f ∈ perms_of_finset s ↔ ∀ {x : α}, ⇑f x ≠ x → x ∈ s
source
theorem card_perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
(perms_of_finset s).card = (s.card)!
source
def fintype_perm {α : Type u_1} [decidable_eq α] [fintype α] :
fintype (equiv.perm α)

The collection of permutations of a fintype is a fintype.

Equations
source
@[protected, instance]
def equiv.fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
fintype (α ≃ β)
Equations
source
theorem fintype.card_perm {α : Type u_1} [decidable_eq α] [fintype α] :
fintype.card (equiv.perm α) = (fintype.card α)!
source
theorem fintype.card_equiv {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] (e : α ≃ β) :
fintype.card (α ≃ β) = (fintype.card α)!
source
theorem univ_eq_singleton_of_card_one {α : Type u_1} [fintype α] (x : α) (h : fintype.card α = 1) :
finset.univ = {x}
source
def fintype.choose_x {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :
{a // p a}

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of the corresponding subtype.

Equations
source
def fintype.choose {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :
α

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of α.

Equations
source
theorem fintype.choose_spec {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :
p (fintype.choose p hp)
source
@[simp]
theorem fintype.choose_subtype_eq {α : Type u_1} (p : α → Prop) [fintype {a // p a}] [decidable_eq α] (x : {a // p a}) (h : (∃! (a : {a // p a}), ↑a = ↑x) := _) :
fintype.choose (λ (y : {a // p a}), ↑y = ↑x) h = x
source
def fintype.bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) (b : β) :
α

bij_inv f is the unique inverse to a bijection f. This acts as a computable alternative to function.inv_fun.

Equations
source
theorem fintype.left_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
function.left_inverse (fintype.bij_inv f_bij) f
source
theorem fintype.right_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
function.right_inverse (fintype.bij_inv f_bij) f
source
theorem fintype.bijective_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
function.bijective (fintype.bij_inv f_bij)
source
theorem fintype.well_founded_of_trans_of_irrefl {α : Type u_1} [fintype α] (r : α → α → Prop) [is_trans α r] [is_irrefl α r] :
well_founded r
source
theorem fintype.preorder.well_founded {α : Type u_1} [fintype α] [preorder α] :
well_founded has_lt.lt
source
@[instance]
theorem fintype.linear_order.is_well_order {α : Type u_1} [fintype α] [linear_order α] :
is_well_order α has_lt.lt
source
@[class]
structure infinite (α : Type u_4) :
Prop

A type is said to be infinite if it has no fintype instance. Note that infinite α is equivalent to is_empty (fintype α).

Instances
source
theorem not_fintype (α : Type u_1) [h1 : infinite α] [h2 : fintype α] :
false
source
@[protected]
theorem fintype.false {α : Type u_1} [infinite α] (h : fintype α) :
false
source
@[protected]
theorem infinite.false {α : Type u_1} [fintype α] (h : infinite α) :
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.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 {α : Type u_1} {β : Type u_2} [infinite β] (f : β → α) (hf : function.injective f) :
infinite α
source
theorem infinite.of_surjective {α : Type u_1} {β : Type 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 infinite.set {α : Type u_1} [infinite α] :
infinite (set α)
source
@[protected, instance]
def finset.infinite {α : Type u_1} [infinite α] :
infinite (finset α)
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 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
@[simp]
theorem infinite_sum {α : Type u_1} {β : Type u_2} :
infinite (α ⊕ β) ↔ 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
@[simp]
theorem infinite_prod {α : Type u_1} {β : Type u_2} :
infinite (α × β) ↔ infinite α ∧ nonempty β ∨ 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
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_fintype {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] (f : α → β) :
¬function.injective f
source
theorem fintype.exists_ne_map_eq_of_infinite {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] (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, fintype.exists_infinite_fiber.

source
@[protected, instance]
def function.embedding.is_empty {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] :
is_empty (α ↪ β)
source
@[protected, instance]
noncomputable def function.embedding.fintype' {α : Type u_1} {β : Type u_2} [fintype β] :
fintype (α ↪ β)
Equations
source
theorem fintype.exists_infinite_fiber {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] (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: fintype.exists_ne_map_eq_of_infinite

source
theorem not_surjective_fintype_infinite {α : Type u_1} {β : Type u_2} [fintype α] [infinite β] (f : α → β) :
¬function.surjective f
source
def trunc_of_multiset_exists_mem {α : Type u_1} (s : multiset α) :
(∃ (x : α), x ∈ s) → trunc α

For s : multiset α, we can lift the existential statement that ∃ x, x ∈ s to a trunc α.

Equations
source
def trunc_of_nonempty_fintype (α : Type u_1) [nonempty α] [fintype α] :
trunc α

A nonempty fintype constructively contains an element.

Equations
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
def trunc_sigma_of_exists {α : Type u_1} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ (a : α), P a) :
trunc (Σ' (a : α), P a)

By iterating over the elements of a fintype, we can lift an existential statement ∃ a, P a to trunc (Σ' a, P a), containing data.

Equations
source
@[simp]
theorem multiset.count_univ {α : Type u_1} [fintype α] [decidable_eq α] (a : α) :
multiset.count a finset.univ.val = 1
source
def fintype.trunc_rec_empty_option {P : Type u → Sort v} (of_equiv : Π {α β : Type u}, α ≃ β → P α → P β) (h_empty : P pempty) (h_option : Π {α : Type u} [_inst_1 : fintype α] [_inst_2 : decidable_eq α], P α → P (option α)) (α : Type u) [fintype α] [decidable_eq α] :
trunc (P α)

A recursor principle for finite types, analogous to nat.rec. It effectively says that every fintype is either empty or option α, up to an equiv.

Equations
source
theorem fintype.induction_empty_option' {P : Π (α : Type u) [_inst_1 : fintype α], Prop} (of_equiv : ∀ (α β : Type u) [_inst_2 : fintype β] (e : α ≃ β), P α → P β) (h_empty : P pempty) (h_option : ∀ (α : Type u) [_inst_3 : fintype α], P α → P (option α)) (α : Type u) [fintype α] :
P α

An induction principle for finite types, analogous to nat.rec. It effectively says that every fintype is either empty or option α, up to an equiv.

source
theorem fintype.induction_empty_option {P : Type u → Prop} (of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β) (h_empty : P pempty) (h_option : ∀ {α : Type u} [_inst_1 : fintype α], P α → P (option α)) (α : Type u) [fintype α] :
P α

An induction principle for finite types, analogous to nat.rec. It effectively says that every fintype is either empty or option α, up to an equiv.

source
noncomputable def seq_of_forall_finset_exists_aux {α : Type u_1} [decidable_eq α] (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : finset α), ∃ (y : α), (∀ (x : α), x ∈ s → P x) → (P y ∧ ∀ (x : α), x ∈ s → r x y)) :
ℕ → α

Auxiliary definition to show exists_seq_of_forall_finset_exists.

Equations
source
theorem exists_seq_of_forall_finset_exists {α : Type u_1} (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : finset α), (∀ (x : α), x ∈ s → P x) → (∃ (y : α), P y ∧ ∀ (x : α), x ∈ s → r x y)) :
∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Induction principle to build a sequence, by adding one point at a time satisfying a given relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set s, one can find another point satisfying some relation r with respect to all the points in s. Then one may construct a function f : ℕ → α such that r (f m) (f n) holds whenever m < n. We also ensure that all constructed points satisfy a given predicate P.

source
theorem exists_seq_of_forall_finset_exists' {α : Type u_1} (P : α → Prop) (r : α → α → Prop) [is_symm α r] (h : ∀ (s : finset α), (∀ (x : α), x ∈ s → P x) → (∃ (y : α), P y ∧ ∀ (x : α), x ∈ s → r x y)) :
∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m ≠ n → r (f m) (f n)

Induction principle to build a sequence, by adding one point at a time satisfying a given symmetric relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set s, one can find another point satisfying some relation r with respect to all the points in s. Then one may construct a function f : ℕ → α such that r (f m) (f n) holds whenever m ≠ n. We also ensure that all constructed points satisfy a given predicate P.

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.