mathlib documentation

data.fintype.basic

@[class]
structure fintype  :
Type u_4Type 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
def finset.univ {α : Type u_1} [fintype α] :

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

Equations
@[simp]
theorem finset.mem_univ {α : Type u_1} [fintype α] (x : α) :

@[simp]
theorem finset.mem_univ_val {α : Type u_1} [fintype α] (x : α) :

@[simp]
theorem finset.coe_univ {α : Type u_1} [fintype α] :

theorem finset.univ_nonempty {α : Type u_1} [fintype α] [nonempty α] :

theorem finset.univ_eq_empty {α : Type u_1} [fintype α] :

theorem finset.subset_univ {α : Type u_1} [fintype α] (s : finset α) :

theorem finset.compl_eq_univ_sdiff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

@[simp]
theorem finset.mem_compl {α : Type u_1} [fintype α] [decidable_eq α] {s : finset α} {x : α} :
x s x s

@[simp]
theorem finset.coe_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

theorem finset.eq_univ_iff_forall {α : Type u_1} [fintype α] {s : finset α} :
s = finset.univ ∀ (x : α), x s

@[simp]
theorem finset.univ_inter {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

@[simp]
theorem finset.inter_univ {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

@[simp]
theorem finset.piecewise_univ {α : Type u_1} [fintype α] [Π (i : α), decidable (i finset.univ)] {δ : α → Sort u_2} (f g : Π (i : α), δ i) :

theorem finset.univ_map_equiv_to_embedding {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (e : α β) :

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

Equations
@[instance]
def fintype.decidable_forall_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :
decidable (∀ (a : α), p a)

Equations
@[instance]
def fintype.decidable_exists_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :
decidable (∃ (a : α), p a)

Equations
@[instance]
def fintype.decidable_eq_equiv_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :

Equations
@[instance]

Equations
@[instance]
def fintype.decidable_left_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] (f : α → β) (g : β → α) :

Equations
@[instance]
def fintype.decidable_right_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype β] (f : α → β) (g : β → α) :

Equations
def fintype.of_multiset {α : Type u_1} [decidable_eq α] (s : multiset α) :
(∀ (x : α), x s)fintype α

Construct a proof of fintype α from a universal multiset

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

Construct a proof of fintype α from a universal list

Equations
theorem fintype.exists_univ_list (α : Type u_1) [fintype α] :
∃ (l : list α), l.nodup ∀ (x : α), x l

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

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

Equations
def fintype.equiv_fin_of_forall_mem_list {α : Type u_1} [decidable_eq α] {l : list α} :
(∀ (x : α), x l)l.nodupα fin l.length

If l lists all the elements of α without duplicates, then α ≃ fin (l.length).

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

There is (computably) a bijection between α and fin n where n = card α. 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.

Equations
theorem fintype.exists_equiv_fin (α : Type u_1) [fintype α] :
∃ (n : ), nonempty fin n)

@[instance]
def fintype.subsingleton (α : Type u_1) :

def fintype.subtype {α : Type u_1} {p : α → Prop} (s : finset α) :
(∀ (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
theorem fintype.subtype_card {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x s p x) :
fintype.card {x // p x} = s.card

theorem fintype.card_of_subtype {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x s p x) [fintype {x // p x}] :
fintype.card {x // p x} = s.card

def fintype.of_finset {α : Type u_1} {p : set α} (s : finset α) :
(∀ (x : α), x s x p)fintype p

Construct a fintype from a finset with the same elements.

Equations
@[simp]
theorem fintype.card_of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x s x p) :

theorem fintype.card_of_finset' {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x s x p) [fintype p] :

def fintype.of_bijective {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) :

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

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

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

Equations
def fintype.of_injective {α : Type u_1} {β : Type u_2} [fintype β] (f : α → β) :

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
def fintype.of_equiv {β : Type u_2} (α : Type u_1) [fintype α] :
α βfintype β

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

Equations
theorem fintype.of_equiv_card {α : Type u_1} {β : Type u_2} [fintype α] (f : α β) :

theorem fintype.card_congr {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
α βfintype.card α = fintype.card β

theorem fintype.card_eq {α : Type u_1} {β : Type u_2} [F : fintype α] [G : fintype β] :

def fintype.of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

Subsingleton types are fintypes (with zero or one terms).

Equations
@[simp]
theorem fintype.univ_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

@[simp]
theorem fintype.card_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

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

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

Equations
@[simp]
theorem set.mem_to_finset {α : Type u_1} {s : set α} [fintype s] {a : α} :

@[simp]
theorem set.mem_to_finset_val {α : Type u_1} {s : set α} [fintype s] {a : α} :

@[simp]
theorem set.to_finset_card {α : Type u_1} (s : set α) [fintype s] :

@[simp]
theorem set.coe_to_finset {α : Type u_1} (s : set α) [fintype s] :

@[simp]
theorem set.to_finset_inj {α : Type u_1} {s t : set α} [fintype s] [fintype t] :

theorem finset.card_univ {α : Type u_1} [fintype α] :

theorem finset.eq_univ_of_card {α : Type u_1} [fintype α] (s : finset α) :

theorem finset.card_le_univ {α : Type u_1} [fintype α] (s : finset α) :

theorem finset.card_univ_diff {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :

theorem finset.card_compl {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :

@[instance]
def fin.fintype (n : ) :

Equations
@[simp]
theorem fintype.card_fin (n : ) :

@[simp]
theorem finset.card_fin (n : ) :

theorem fin.equiv_iff_eq {m n : } :
nonempty (fin m fin n) m = n

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

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

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

@[instance]
def unique.fintype {α : Type u_1} [unique α] :

Equations
@[simp]
theorem univ_unique {α : Type u_1} [unique α] [f : fintype α] :

@[instance]

Equations
@[simp]

@[simp]

@[instance]

Equations
@[simp]

@[instance]

Equations
@[simp]

@[instance]

Equations
@[instance]
def additive.fintype {α : Type u_1} [fintype α] :

Equations
@[instance]
def multiplicative.fintype {α : Type u_1} [fintype α] :

Equations
@[instance]
def units.fintype {α : Type u_1} [monoid α] [fintype α] :

Equations
@[simp]

def finset.insert_none {α : Type u_1} :
finset αfinset (option α)

Given a finset on α, lift it to being a finset on option α using option.some and then insert option.none.

Equations
@[simp]
theorem finset.mem_insert_none {α : Type u_1} {s : finset α} {o : option α} :
o s.insert_none ∀ (a : α), a oa s

theorem finset.some_mem_insert_none {α : Type u_1} {s : finset α} {a : α} :

@[instance]
def option.fintype {α : Type u_1} [fintype α] :

Equations
@[simp]
theorem fintype.card_option {α : Type u_1} [fintype α] :

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

Equations
@[simp]
theorem finset.univ_sigma_univ {α : Type u_1} {β : α → Type u_2} [fintype α] [Π (a : α), fintype (β a)] :

@[instance]
def prod.fintype (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
fintype × β)

Equations
@[simp]
theorem finset.univ_product_univ {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :

@[simp]
theorem fintype.card_prod (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :

def fintype.fintype_prod_left {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype × β)] [nonempty β] :

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

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

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

Equations
@[instance]
def ulift.fintype (α : Type u_1) [fintype α] :

Equations
@[simp]
theorem fintype.card_ulift (α : Type u_1) [fintype α] :

@[instance]
def sum.fintype (α : Type u) (β : Type v) [fintype α] [fintype β] :
fintype β)

Equations
theorem fintype.card_le_of_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :

theorem fintype.exists_ne_map_eq_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :
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.

theorem fintype.card_eq_one_iff {α : Type u_1} [fintype α] :
fintype.card α = 1 ∃ (x : α), ∀ (y : α), y = x

theorem fintype.card_eq_zero_iff {α : Type u_1} [fintype α] :
fintype.card α = 0 α → false

A fintype with cardinality zero is (constructively) equivalent to pempty.

Equations
theorem fintype.card_pos_iff {α : Type u_1} [fintype α] :

theorem fintype.card_le_one_iff {α : Type u_1} [fintype α] :
fintype.card α 1 ∀ (a b : α), a = b

theorem fintype.exists_ne_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < fintype.card α) (a : α) :
∃ (b : α), b a

theorem fintype.exists_pair_of_one_lt_card {α : Type u_1} [fintype α] :
1 < fintype.card α(∃ (a b : α), a b)

theorem fintype.injective_iff_surjective {α : Type u_1} [fintype α] {f : α → α} :

theorem fintype.injective_iff_bijective {α : Type u_1} [fintype α] {f : α → α} :

theorem fintype.surjective_iff_bijective {α : Type u_1} [fintype α] {f : α → α} :

theorem fintype.injective_iff_surjective_of_equiv {α : Type u_1} [fintype α] {β : Type u_2} {f : α → β} :

theorem fintype.nonempty_equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :

theorem fintype.bijective_iff_injective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :

theorem fintype.bijective_iff_surjective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :

theorem fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} :

@[instance]
def list.subtype.fintype {α : Type u_1} [decidable_eq α] (l : list α) :
fintype {x // x l}

Equations
@[instance]
def multiset.subtype.fintype {α : Type u_1} [decidable_eq α] (s : multiset α) :
fintype {x // x s}

Equations
@[instance]
def finset.subtype.fintype {α : Type u_1} (s : finset α) :
fintype {x // x s}

Equations
@[instance]
def finset_coe.fintype {α : Type u_1} (s : finset α) :

Equations
@[simp]
theorem fintype.card_coe {α : Type u_1} (s : finset α) :

theorem finset.attach_eq_univ {α : Type u_1} {s : finset α} :

theorem finset.card_le_one_iff {α : Type u_1} {s : finset α} :
s.card 1 ∀ {x y : α}, x sy sx = y

theorem finset.card_le_one_of_subsingleton {α : Type u_1} [subsingleton α] (s : finset α) :
s.card 1

A finset of a subsingleton type has cardinality at most one.

theorem finset.one_lt_card_iff {α : Type u_1} {s : finset α} :
1 < s.card ∃ (x y : α), x s y s x y

@[instance]
def plift.fintype (p : Prop) [decidable p] :

Equations
@[instance]
def Prop.fintype  :
fintype Prop

Equations
@[instance]
def subtype.fintype {α : Type u_1} (p : α → Prop) [decidable_pred p] [fintype α] :
fintype {x // p x}

Equations
def set_fintype {α : Type u_1} [fintype α] (s : set α) [decidable_pred s] :

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

Equations
def function.embedding.equiv_of_fintype_self_embedding {α : Type u_1} [fintype α] :
α)α α

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

Equations
@[simp]
theorem finset.univ_map_embedding {α : Type u_1} [fintype α] (e : α α) :

def fintype.pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} :
(Π (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
@[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

theorem fintype.pi_finset_subset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (t₁ t₂ : Π (a : α), finset (δ a)) :
(∀ (a : α), t₁ a t₂ a)fintype.pi_finset t₁ fintype.pi_finset t₂

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 : α} :
disjoint (t₁ a) (t₂ a)disjoint (fintype.pi_finset t₁) (fintype.pi_finset t₂)

pi

@[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
@[simp]
theorem fintype.pi_finset_univ {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :

@[instance]
def d_array.fintype {n : } {α : fin nType u_1} [Π (n : fin n), fintype (α n)] :

Equations
@[instance]
def array.fintype {n : } {α : Type u_1} [fintype α] :
fintype (array n α)

Equations
@[instance]
def vector.fintype {α : Type u_1} [fintype α] {n : } :

Equations
@[instance]
def finset.fintype {α : Type u_1} [fintype α] :

Equations
@[simp]
theorem fintype.card_finset {α : Type u_1} [fintype α] :

@[simp]
theorem set.to_finset_univ {α : Type u_1} [fintype α] :

@[simp]
theorem set.to_finset_empty {α : Type u_1} [fintype α] :

theorem fintype.card_subtype_le {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :

theorem fintype.card_subtype_lt {α : Type u_1} [fintype α] {p : α → Prop} [decidable_pred p] {x : α} :
¬p xfintype.card {x // p x} < fintype.card α

@[instance]
def psigma.fintype {α : Type u_1} {β : α → Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)

Equations
@[instance]
def psigma.fintype_prop_left {α : Prop} {β : α → Type u_1} [decidable α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)

Equations
@[instance]
def psigma.fintype_prop_right {α : Type u_1} {β : α → Prop} [Π (a : α), decidable (β a)] [fintype α] :
fintype (Σ' (a : α), β a)

Equations
@[instance]
def psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [Π (a : α), decidable (β a)] :
fintype (Σ' (a : α), β a)

Equations
@[instance]
def set.fintype {α : Type u_1} [fintype α] :

Equations
@[instance]
def pfun_fintype (p : Prop) [decidable p] (α : p → Type u_1) [Π (hp : p), fintype (α hp)] :
fintype (Π (hp : p), α hp)

Equations
@[simp]
theorem finset.univ_pi_univ {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :

theorem mem_image_univ_iff_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} {b : β} :

theorem card_lt_card_of_injective_of_not_mem {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.injective f) {b : β} :

def quotient.fin_choice_aux {ι : Type u_1} [decidable_eq ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) :
(Π (i : ι), i lquotient (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
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

def quotient.fin_choice {ι : Type u_1} [decidable_eq ι] [fintype ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] :
(Π (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
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

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
theorem length_perms_of_list {α : Type u_1} [decidable_eq α] (l : list α) :

theorem mem_perms_of_list_of_mem {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
(∀ (x : α), f x xx l)f perms_of_list l

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 xx l

theorem mem_perms_of_list_iff {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
f perms_of_list l ∀ {x : α}, f x xx l

theorem nodup_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} :

def perms_of_finset {α : Type u_1} [decidable_eq α] :

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

Equations
theorem mem_perms_of_finset_iff {α : Type u_1} [decidable_eq α] {s : finset α} {f : equiv.perm α} :
f perms_of_finset s ∀ {x : α}, f x xx s

theorem card_perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :

def fintype_perm {α : Type u_1} [decidable_eq α] [fintype α] :

The collection of permutations of a fintype is a fintype.

Equations
@[instance]
def equiv.fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
fintype β)

Equations
theorem fintype.card_perm {α : Type u_1} [decidable_eq α] [fintype α] :

theorem fintype.card_equiv {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
α βfintype.card β) = (fintype.card α)!

theorem univ_eq_singleton_of_card_one {α : Type u_1} [fintype α] (x : α) :

def fintype.choose_x {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
(∃! (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
def fintype.choose {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
(∃! (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
theorem fintype.choose_spec {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :

def fintype.bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} :
function.bijective fβ → α

bij_inv fis the unique inverse to a bijectionf. This acts as a computable alternative tofunction.inv_fun`.

Equations
theorem fintype.left_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :

theorem fintype.right_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :

theorem fintype.bijective_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :

theorem fintype.well_founded_of_trans_of_irrefl {α : Type u_1} [fintype α] (r : α → α → Prop) [is_trans α r] [is_irrefl α r] :

@[instance]

@[class]
structure infinite  :
Type u_4 → Prop

A type is said to be infinite if it has no fintype instance.

Instances
@[simp]
theorem not_nonempty_fintype {α : Type u_1} :

theorem finset.exists_minimal {α : Type u_1} [preorder α] (s : finset α) :
s.nonempty(∃ (m : α) (H : m s), ∀ (x : α), x s¬x < m)

theorem finset.exists_maximal {α : Type u_1} [preorder α] (s : finset α) :
s.nonempty(∃ (m : α) (H : m s), ∀ (x : α), x s¬m < x)

theorem infinite.exists_not_mem_finset {α : Type u_1} [infinite α] (s : finset α) :
∃ (x : α), x s

@[instance]
def infinite.nontrivial (α : Type u_1) [H : infinite α] :

theorem infinite.nonempty (α : Type u_1) [infinite α] :

theorem infinite.of_injective {α : Type u_1} {β : Type u_2} [infinite β] (f : β → α) :

theorem infinite.of_surjective {α : Type u_1} {β : Type u_2} [infinite β] (f : α → β) :

def infinite.nat_embedding (α : Type u_1) [infinite α] :
α

Embedding of into an infinite type.

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

theorem not_injective_infinite_fintype {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] (f : α → β) :

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.

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

theorem not_surjective_fintype_infinite {α : Type u_1} {β : Type u_2} [fintype α] [infinite β] (f : α → β) :

@[instance]

@[instance]

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
def trunc_of_nonempty_fintype (α : Type u_1) [nonempty α] [fintype α] :

A nonempty fintype constructively contains an element.

Equations
def trunc_of_card_pos {α : Type u_1} [fintype α] :
0 < fintype.card αtrunc α

A fintype with positive cardinality constructively contains an element.

Equations
def trunc_sigma_of_exists {α : Type u_1} [fintype α] {P : α → Prop} [decidable_pred P] :
(∃ (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