mathlib documentation

data.fintype.basic

@[class]

structure fintype (α : Type u_4) :

Type u_4

elems : finset α
complete : ∀ (x : α), x ∈ fintype.elems α

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

finset.univ = fintype.elems α

@[simp]

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

x ∈ finset.univ

@[simp]

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

x ∈ finset.univ.val

@[simp]

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

↑finset.univ = set.univ

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

s ⊆ finset.univ

@[instance]

def finset.order_top {α : Type u_1} [fintype α] :

order_top (finset α)

Equations

finset.order_top = {top := finset.univ _inst_1, le := partial_order.le finset.partial_order, lt := partial_order.lt finset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

@[instance]

def finset.boolean_algebra {α : Type u_1} [fintype α] [decidable_eq α] :

boolean_algebra (finset α)

Equations

finset.boolean_algebra = {sup := distrib_lattice.sup finset.distrib_lattice, le := distrib_lattice.le finset.distrib_lattice, lt := distrib_lattice.lt finset.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf finset.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := order_top.top finset.order_top, le_top := _, bot := semilattice_inf_bot.bot finset.semilattice_inf_bot, bot_le := _, compl := λ (s : finset α), finset.univ \ s, sdiff := has_sdiff.sdiff finset.has_sdiff, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _}

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

sᶜ = finset.univ \ s

@[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 α) :

↑sᶜ = (↑s)ᶜ

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 α) :

finset.univ ∩ s = s

@[simp]

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

s ∩ finset.univ = s

@[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

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

@[instance]

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

decidable_eq (Π (a : α), β a)

Equations

fintype.decidable_pi_fintype = λ (f g : Π (a : α), β a), decidable_of_iff (∀ (a : α), a ∈ fintype.elems α → f a = g a) _

@[instance]

def fintype.decidable_forall_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :

decidable (∀ (a : α), p a)

Equations

fintype.decidable_forall_fintype = decidable_of_iff (∀ (a : α), a ∈ finset.univ → p a) fintype.decidable_forall_fintype._proof_1

@[instance]

def fintype.decidable_exists_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :

decidable (∃ (a : α), p a)

Equations

fintype.decidable_exists_fintype = decidable_of_iff (∃ (a : α) (H : a ∈ finset.univ), p a) fintype.decidable_exists_fintype._proof_1

@[instance]

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

decidable_eq (α ≃ β)

Equations

fintype.decidable_eq_equiv_fintype = λ (a b : α ≃ β), decidable_of_iff (a.to_fun = b.to_fun) _

@[instance]

def fintype.decidable_injective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] :

decidable_pred function.injective

Equations

fintype.decidable_injective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype

@[instance]

def fintype.decidable_surjective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [fintype β] :

decidable_pred function.surjective

Equations

fintype.decidable_surjective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype

@[instance]

def fintype.decidable_bijective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :

decidable_pred function.bijective

Equations

fintype.decidable_bijective_fintype = λ (x : α → β), _.mpr and.decidable

@[instance]

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

decidable (function.right_inverse f g)

Equations

fintype.decidable_left_inverse_fintype f g = show decidable (∀ (x : α), g (f x) = x), from fintype.decidable_forall_fintype

@[instance]

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

decidable (function.left_inverse f g)

Equations

fintype.decidable_right_inverse_fintype f g = show decidable (∀ (x : β), f (g x) = x), from fintype.decidable_forall_fintype

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

Construct a proof of fintype α from a universal multiset

Equations

fintype.of_multiset s H = {elems := s.to_finset, complete := _}

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

Construct a proof of fintype α from a universal list

Equations

fintype.of_list l H = {elems := l.to_finset, complete := _}

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

fintype.card α = finset.univ.card

def fintype.equiv_fin_of_forall_mem_list {α : Type u_1} [decidable_eq α] {l : list α} (h : ∀ (x : α), x ∈ l) (nd : l.nodup) :

α ≃ fin l.length

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

Equations

fintype.equiv_fin_of_forall_mem_list h nd = {to_fun := λ (a : α), ⟨list.index_of a l, _⟩, inv_fun := λ (i : fin l.length), l.nth_le i.val _, left_inv := _, right_inv := _}

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

trunc (α ≃ fin (fintype.card α))

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

fintype.equiv_fin α = _.mpr (quot.rec_on_subsingleton finset.univ.val (λ (l : list α) (h : ∀ (x : α), x ∈ l) (nd : l.nodup), trunc.mk (fintype.equiv_fin_of_forall_mem_list h nd)) finset.mem_univ_val _)

theorem fintype.exists_equiv_fin (α : Type u_1) [fintype α] :

∃ (n : ℕ), nonempty (α ≃ fin n)

@[instance]

def fintype.subsingleton (α : Type u_1) :

subsingleton (fintype α)

def fintype.subtype {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ p x) :

fintype {x // p x}

Equations

fintype.subtype s H = {elems := {val := multiset.pmap subtype.mk s.val _, nodup := _}, complete := _}

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 α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :

Construct a fintype from a finset with the same elements.

Equations

fintype.of_finset s H = fintype.subtype s H

@[simp]

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

fintype.card ↥p = s.card

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

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

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

Equations

fintype.of_bijective f H = {elems := finset.map {to_fun := f, inj' := _} finset.univ, complete := _}

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

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

Equations

fintype.of_surjective f H = {elems := finset.image f finset.univ, complete := _}

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

Equations

fintype.of_injective f H = let _inst : Π (p : Prop), decidable p := classical.dec in dite (nonempty α) (λ (hα : nonempty α), let _inst_2 : inhabited α := classical.inhabited_of_nonempty hα in fintype.of_surjective (function.inv_fun f) _) (λ (hα : ¬nonempty α), {elems := ∅, complete := _})

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

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

Equations

fintype.of_equiv α f = fintype.of_bijective ⇑f _

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

fintype.card β = fintype.card α

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

fintype.card α = fintype.card β

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

fintype.card α = fintype.card β ↔ nonempty (α ≃ β)

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

Equations

fintype.of_subsingleton a = {elems := {a}, complete := _}

@[simp]

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

finset.univ = {a}

@[simp]

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

fintype.card α = 1

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

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

Equations

s.to_finset = {val := multiset.map subtype.val finset.univ.val, nodup := _}

@[simp]

theorem set.mem_to_finset {α : Type u_1} {s : set α} [fintype ↥s] {a : α} :

a ∈ s.to_finset ↔ a ∈ s

@[simp]

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

a ∈ s.to_finset.val ↔ a ∈ s

@[simp]

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

s.to_finset.card = fintype.card ↥s

@[simp]

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

↑(s.to_finset) = s

@[simp]

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

s.to_finset = t.to_finset ↔ s = t

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

finset.univ.card = fintype.card α

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

s = finset.univ

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

s.card ≤ fintype.card α

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

(finset.univ \ s).card = fintype.card α - s.card

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

sᶜ.card = fintype.card α - s.card

@[instance]

def fin.fintype (n : ℕ) :

fintype (fin n)

Equations

fin.fintype n = {elems := finset.fin_range n, complete := _}

@[simp]

theorem fintype.card_fin (n : ℕ) :

fintype.card (fin n) = n

@[simp]

theorem finset.card_fin (n : ℕ) :

finset.univ.card = n

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

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

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

@[instance]

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

Equations

unique.fintype = fintype.of_subsingleton (default α)

@[simp]

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

finset.univ = {default α}

@[instance]

def empty.fintype :

Equations

empty.fintype = {elems := ∅, complete := empty.fintype._proof_1}

@[simp]

theorem fintype.univ_empty :

finset.univ = ∅

@[simp]

theorem fintype.card_empty :

fintype.card empty = 0

@[instance]

def pempty.fintype :

Equations

pempty.fintype = {elems := ∅, complete := pempty.fintype._proof_1}

@[simp]

theorem fintype.univ_pempty :

finset.univ = ∅

@[simp]

theorem fintype.card_pempty :

fintype.card pempty = 0

@[instance]

def unit.fintype :

Equations

unit.fintype = fintype.of_subsingleton ()

theorem fintype.univ_unit :

finset.univ = {()}

theorem fintype.card_unit :

fintype.card unit = 1

@[instance]

def punit.fintype :

Equations

punit.fintype = fintype.of_subsingleton punit.star

@[simp]

theorem fintype.univ_punit :

finset.univ = {punit.star}

@[simp]

theorem fintype.card_punit :

fintype.card punit = 1

@[instance]

def bool.fintype :

Equations

bool.fintype = {elems := {val := tt :: ff :: 0, nodup := bool.fintype._proof_1}, complete := bool.fintype._proof_2}

@[simp]

theorem fintype.univ_bool :

finset.univ = {tt, ff}

@[instance]

def units_int.fintype :

fintype (units ℤ)

Equations

units_int.fintype = {elems := {1, -1}, complete := units_int.fintype._proof_1}

@[instance]

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

fintype (additive α)

Equations

additive.fintype = id

@[instance]

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

fintype (multiplicative α)

Equations

multiplicative.fintype = id

@[simp]

theorem fintype.card_units_int :

fintype.card (units ℤ) = 2

@[instance]

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

fintype (units α)

Equations

units.fintype = fintype.of_injective units.val units.ext

@[simp]

theorem fintype.card_bool :

fintype.card bool = 2

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

finset (option α)

Equations

s.insert_none = {val := none :: multiset.map some s.val, nodup := _}

@[simp]

theorem finset.mem_insert_none {α : Type u_1} {s : finset α} {o : option α} :

o ∈ s.insert_none ↔ ∀ (a : α), a ∈ o → a ∈ s

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

some a ∈ s.insert_none ↔ a ∈ s

@[instance]

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

fintype (option α)

Equations

option.fintype = {elems := finset.univ.insert_none, complete := _}

@[simp]

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

fintype.card (option α) = fintype.card α + 1

@[instance]

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

fintype (sigma β)

Equations

sigma.fintype β = {elems := finset.univ.sigma (λ (_x : α), finset.univ), complete := _}

@[simp]

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

finset.univ.sigma (λ (a : α), finset.univ) = finset.univ

@[instance]

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

fintype (α × β)

Equations

prod.fintype α β = {elems := finset.univ.product finset.univ, complete := _}

@[simp]

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

finset.univ.product finset.univ = finset.univ

@[simp]

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

fintype.card (α × β) = (fintype.card α) * fintype.card β

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

Equations

fintype.fintype_prod_left = {elems := finset.image prod.fst (fintype.elems (α × β)), complete := _}

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

Equations

fintype.fintype_prod_right = {elems := finset.image prod.snd (fintype.elems (α × β)), complete := _}

@[instance]

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

fintype (ulift α)

Equations

ulift.fintype α = fintype.of_equiv α equiv.ulift.symm

@[simp]

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

fintype.card (ulift α) = fintype.card α

@[instance]

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

fintype (α ⊕ β)

Equations

sum.fintype α β = fintype.of_equiv (Σ (b : bool), cond b (ulift α) (ulift β)) ((equiv.sum_equiv_sigma_bool (ulift α) (ulift β)).symm.trans (equiv.ulift.sum_congr equiv.ulift))

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

fintype.card α ≤ fintype.card β

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

def fintype.card_eq_zero_equiv_equiv_pempty {α : Type u_1} [fintype α] :

fintype.card α = 0 ≃ (α ≃ pempty)

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

Equations

fintype.card_eq_zero_equiv_equiv_pempty = {to_fun := λ (h : fintype.card α = 0), {to_fun := λ (a : α), _.elim, inv_fun := λ (a : pempty), a.elim, left_inv := _, right_inv := _}, inv_fun := _, left_inv := _, right_inv := _}

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

0 < fintype.card α ↔ nonempty α

theorem fintype.card_le_one_iff {α : Type u_1} [fintype α] :

fintype.card α ≤ 1 ↔ ∀ (a b : α), a = b

theorem fintype.card_le_one_iff_subsingleton {α : Type u_1} [fintype α] :

fintype.card α ≤ 1 ↔ subsingleton α

theorem fintype.one_lt_card_iff_nontrivial {α : Type u_1} [fintype α] :

1 < fintype.card α ↔ nontrivial α

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 α] (h : 1 < fintype.card α) :

∃ (a b : α), a ≠ b

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

function.injective f ↔ function.surjective f

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

function.injective f ↔ function.bijective f

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

function.surjective f ↔ function.bijective f

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

function.injective f ↔ function.surjective f

theorem fintype.nonempty_equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : fintype.card α = fintype.card β) :

nonempty (α ≃ β)

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 β

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 β

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

↑(finset.image f finset.univ) = set.range f

@[instance]

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

fintype {x // x ∈ l}

Equations

list.subtype.fintype l = fintype.of_list l.attach _

@[instance]

def multiset.subtype.fintype {α : Type u_1} [decidable_eq α] (s : multiset α) :

fintype {x // x ∈ s}

Equations

multiset.subtype.fintype s = fintype.of_multiset s.attach _

@[instance]

def finset.subtype.fintype {α : Type u_1} (s : finset α) :

fintype {x // x ∈ s}

Equations

finset.subtype.fintype s = {elems := s.attach, complete := _}

@[instance]

def finset_coe.fintype {α : Type u_1} (s : finset α) :

fintype ↥↑s

Equations

finset_coe.fintype s = finset.subtype.fintype s

@[simp]

theorem fintype.card_coe {α : Type u_1} (s : finset α) :

fintype.card ↥↑s = s.card

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

s.attach = finset.univ

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

s.card ≤ 1 ↔ ∀ {x y : α}, x ∈ s → y ∈ s → x = y

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

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] :

fintype (plift p)

Equations

plift.fintype p = {elems := dite p (λ (h : p), {{down := h}}) (λ (h : ¬p), ∅), complete := _}

@[instance]

def Prop.fintype :

Equations

Prop.fintype = {elems := {val := true :: false :: 0, nodup := Prop.fintype._proof_1}, complete := Prop.fintype._proof_2}

@[instance]

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

fintype {x // p x}

Equations

subtype.fintype p = fintype.subtype (finset.filter p finset.univ) _

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

Equations

set_fintype s = subtype.fintype (λ (x : α), x ∈ s)

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

e.equiv_of_fintype_self_embedding = equiv.of_bijective ⇑e _

@[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

@[simp]

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

finset.map e finset.univ = finset.univ

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

fintype.pi_finset t = finset.map {to_fun := λ (f : Π (a : α), a ∈ finset.univ → δ a) (a : α), f a _, inj' := _} (finset.univ.pi t)

@[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)) (h : ∀ (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 : α} (h : 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

pi.fintype = {elems := fintype.pi_finset (λ (_x : α), finset.univ), complete := _}

@[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

@[instance]

def d_array.fintype {n : ℕ} {α : fin n → Type u_1} [Π (n : fin n), fintype (α n)] :

fintype (d_array n α)

Equations

d_array.fintype = fintype.of_equiv (Π (i : fin n), α i) (equiv.d_array_equiv_fin α).symm

@[instance]

def array.fintype {n : ℕ} {α : Type u_1} [fintype α] :

fintype (array n α)

Equations

array.fintype = d_array.fintype

@[instance]

def vector.fintype {α : Type u_1} [fintype α] {n : ℕ} :

fintype (vector α n)

Equations

vector.fintype = fintype.of_equiv (fin n → α) (equiv.vector_equiv_fin α n).symm

@[instance]

def quotient.fintype {α : Type u_1} [fintype α] (s : setoid α) [decidable_rel has_equiv.equiv] :

fintype (quotient s)

Equations

quotient.fintype s = fintype.of_surjective quotient.mk _

@[instance]

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

fintype (finset α)

Equations

finset.fintype = {elems := finset.univ.powerset, complete := _}

@[simp]

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

fintype.card (finset α) = 2 ^ fintype.card α

@[simp]

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

set.univ.to_finset = finset.univ

@[simp]

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

∅.to_finset = ∅

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

fintype.card {x // p x} ≤ fintype.card α

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 α

@[instance]

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

fintype (Σ' (a : α), β a)

Equations

psigma.fintype = fintype.of_equiv (Σ (i : α), β i) (equiv.psigma_equiv_sigma (λ (a : α), β a)).symm

@[instance]

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

fintype (Σ' (a : α), β a)

Equations

psigma.fintype_prop_left = dite α (λ (h : α), fintype.of_equiv (β h) {to_fun := λ (x : β h), ⟨h, x⟩, inv_fun := psigma.snd (λ (a : α), β a), left_inv := _, right_inv := _}) (λ (h : ¬α), {elems := ∅, complete := _})

@[instance]

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

fintype (Σ' (a : α), β a)

Equations

psigma.fintype_prop_right = fintype.of_equiv {a // β a} {to_fun := λ (_x : {a // β a}), psigma.fintype_prop_right._match_1 _x, inv_fun := λ (_x : Σ' (a : α), β a), psigma.fintype_prop_right._match_2 _x, left_inv := _, right_inv := _}
psigma.fintype_prop_right._match_1 ⟨x, y⟩ = ⟨x, y⟩
psigma.fintype_prop_right._match_2 ⟨x, y⟩ = ⟨x, y⟩

@[instance]

def psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [Π (a : α), decidable (β a)] :

fintype (Σ' (a : α), β a)

Equations

psigma.fintype_prop_prop = dite (∃ (a : α), β a) (λ (h : ∃ (a : α), β a), {elems := {⟨_, _⟩}, complete := _}) (λ (h : ¬∃ (a : α), β a), {elems := ∅, complete := _})

@[instance]

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

fintype (set α)

Equations

set.fintype = {elems := finset.map {to_fun := coe lift_base, inj' := _} finset.univ.powerset, complete := _}

@[instance]

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

fintype (Π (hp : p), α hp)

Equations

pfun_fintype p α = dite p (λ (hp : p), fintype.of_equiv (α hp) {to_fun := λ (a : α hp) (_x : p), a, inv_fun := λ (f : Π (hp : p), α hp), f hp, left_inv := _, right_inv := _}) (λ (hp : ¬p), {elems := {λ (h : p), _.elim}, complete := _})

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

theorem card_lt_card_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 β

def quotient.fin_choice_aux {ι : Type u_1} [decidable_eq ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) (a : Π (i : ι), i ∈ l → quotient (S i)) :

quotient pi_setoid

Equations

quotient.fin_choice_aux (i :: l) f = (f i _).lift_on₂ (quotient.fin_choice_aux l (λ (j : ι) (h : j ∈ l), f j _)) (λ (a : α i) (l_1 : Π (i : ι), i ∈ l → α i), ⟦(λ (j : ι) (h : j ∈ i :: l), dite (j = i) (λ (e : j = i), _.mpr a) (λ (e : ¬j = i), l_1 j _))⟧) _
quotient.fin_choice_aux list.nil f = ⟦(λ (i : ι), false.elim)⟧

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)] (f : Π (i : ι), quotient (S i)) :

quotient pi_setoid

Equations

quotient.fin_choice f = quotient.lift_on (quotient.rec_on finset.univ.val (λ (l : list ι), quotient.fin_choice_aux l (λ (i : ι) (_x : i ∈ l), f i)) _) (λ (f : Π (i : ι), i ∈ finset.univ.val → α i), ⟦(λ (i : ι), f i _)⟧) quotient.fin_choice._proof_2

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 α] (a : list α) :

list (equiv.perm α)

Equations

perms_of_list (a :: l) = perms_of_list l ++ l.bind (λ (b : α), list.map (λ (f : equiv.perm α), (equiv.swap a b) * f) (perms_of_list l))
perms_of_list list.nil = [1]

theorem length_perms_of_list {α : Type u_1} [decidable_eq α] (l : list α) :

(perms_of_list l).length = l.length.fact

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

theorem mem_of_mem_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} (a : f ∈ perms_of_list l) {x : α} (a_1 : ⇑f x ≠ x) :

x ∈ 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 ≠ x → x ∈ l

theorem nodup_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) :

(perms_of_list l).nodup

def perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :

finset (equiv.perm α)

Equations

perms_of_finset s = quotient.hrec_on s.val (λ (l : list α) (hl : multiset.nodup ⟦l⟧), {val := ↑(perms_of_list l), nodup := _}) perms_of_finset._proof_2 _

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

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

(perms_of_finset s).card = s.card.fact

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

fintype (equiv.perm α)

Equations

fintype_perm = {elems := perms_of_finset finset.univ, complete := _}

@[instance]

def equiv.fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :

fintype (α ≃ β)

Equations

equiv.fintype = dite (fintype.card β = fintype.card α) (λ (h : fintype.card β = fintype.card α), (fintype.equiv_fin α).rec_on_subsingleton (λ (eα : α ≃ fin (fintype.card α)), (fintype.equiv_fin β).rec_on_subsingleton (λ (eβ : β ≃ fin (fintype.card β)), fintype.of_equiv (equiv.perm α) ((equiv.refl α).equiv_congr (eα.trans (h.rec_on eβ.symm)))))) (λ (h : ¬fintype.card β = fintype.card α), {elems := ∅, complete := _})

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

fintype.card (equiv.perm α) = (fintype.card α).fact

theorem fintype.card_equiv {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] (e : α ≃ β) :

fintype.card (α ≃ β) = (fintype.card α).fact

theorem univ_eq_singleton_of_card_one {α : Type u_1} [fintype α] (x : α) (h : fintype.card α = 1) :

finset.univ = {x}

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

{a // p a}

Equations

fintype.choose_x p hp = ⟨finset.choose p finset.univ _, _⟩

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

α

Equations

fintype.choose p hp = ↑(fintype.choose_x p hp)

theorem fintype.choose_spec {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :

p (fintype.choose p hp)

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

α

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

Equations

fintype.bij_inv f_bij b = fintype.choose (λ (a : α), f a = b) _

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

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

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)

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

theorem fintype.preorder.well_founded {α : Type u_1} [fintype α] [preorder α] :

well_founded has_lt.lt

@[instance]

theorem fintype.linear_order.is_well_order {α : Type u_1} [fintype α] [linear_order α] :

is_well_order α has_lt.lt

@[class]

structure infinite (α : Type u_4) :

Prop

not_fintype : fintype α → false

Instances

@[simp]

theorem not_nonempty_fintype {α : Type u_1} :

¬nonempty (fintype α) ↔ infinite α

theorem finset.exists_minimal {α : Type u_1} [preorder α] (s : finset α) (h : s.nonempty) :

∃ (m : α) (H : m ∈ s), ∀ (x : α), x ∈ s → ¬x < m

theorem finset.exists_maximal {α : Type u_1} [preorder α] (s : finset α) (h : s.nonempty) :

∃ (m : α) (H : m ∈ s), ∀ (x : α), x ∈ s → ¬m < x

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

∃ (x : α), x ∉ s

@[instance]

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

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

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

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

Embedding of ℕ into an infinite type.

Equations

infinite.nat_embedding α = {to_fun := nat_embedding_aux α _inst_1, inj' := _}

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 : α → β) :

¬function.injective f

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

¬function.surjective f

@[instance]

def nat.infinite :

@[instance]

def int.infinite :

def trunc_of_multiset_exists_mem {α : Type u_1} (s : multiset α) (a : ∃ (x : α), x ∈ s) :

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

Equations

trunc_of_multiset_exists_mem s = quotient.rec_on_subsingleton s (λ (l : list α) (h : ∃ (x : α), x ∈ ⟦l⟧), trunc_of_multiset_exists_mem._match_1 l h l h)
trunc_of_multiset_exists_mem._match_1 l h (a :: _x) _x_1 = trunc.mk a
trunc_of_multiset_exists_mem._match_1 l h list.nil _x = false.elim _

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

A nonempty fintype constructively contains an element.

Equations

trunc_of_nonempty_fintype α = trunc_of_multiset_exists_mem finset.univ.val _

def trunc_of_card_pos {α : Type u_1} [fintype α] (h : 0 < fintype.card α) :

A fintype with positive cardinality constructively contains an element.

Equations

trunc_of_card_pos h = let _inst : nonempty α := _ in trunc_of_nonempty_fintype α

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

trunc_sigma_of_exists h = trunc_of_nonempty_fintype (Σ' (a : α), P a)