mathlib3 documentation

data.fintype.basic

Finite types #

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

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

Main declarations #

See data.fintype.card for the cardinality of a fintype, the equivalence with fin (fintype.card α), and pigeonhole principles.

Instances #

Instances for fintype for

These files also contain appropriate infinite instances for these types.

infinite instances for ℕ, ℤ, multiset α, and list α are in data.fintype.lattice.

Types which have a surjection from/an injection to a fintype are themselves fintypes. See fintype.of_injective and fintype.of_surjective.

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 of this typeclass
Instances of other typeclasses for fintype
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
theorem finset.eq_univ_of_forall {α : Type u_1} [fintype α] {s : finset α} :
(∀ (x : α), x ∈ s) → s = finset.univ
source
@[simp, norm_cast]
theorem finset.coe_univ {α : Type u_1} [fintype α] :
↑finset.univ = set.univ
source
@[simp, norm_cast]
theorem finset.coe_eq_univ {α : Type u_1} [fintype α] {s : finset α} :
↑s = set.univ ↔ s = finset.univ
source
theorem finset.nonempty.eq_univ {α : Type u_1} [fintype α] {s : finset α} [subsingleton α] :
s.nonempty → s = finset.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 = {inhabited.default}
source
@[simp]
theorem finset.subset_univ {α : Type u_1} [fintype α] (s : finset α) :
s ⊆ finset.univ
source
@[protected, instance]
def finset.bounded_order {α : Type u_1} [fintype α] :
bounded_order (finset α)
Equations
source
@[simp]
theorem finset.top_eq_univ {α : Type u_1} [fintype α] :
⊤ = finset.univ
source
theorem finset.ssubset_univ_iff {α : Type u_1} [fintype α] {s : finset α} :
s ⊂ finset.univ ↔ s ≠ finset.univ
source
theorem finset.codisjoint_left {α : Type u_1} [fintype α] {s t : finset α} :
codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t
source
theorem finset.codisjoint_right {α : Type u_1} [fintype α] {s t : finset α} :
codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s
source
@[protected, instance]
def finset.boolean_algebra {α : Type u_1} [fintype α] [decidable_eq α] :
boolean_algebra (finset α)
Equations
source
theorem finset.sdiff_eq_inter_compl {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :
s \ t = s ∩ tᶜ
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 α] {s : finset α} [decidable_eq α] {a : α} :
a ∈ sᶜ ↔ a ∉ s
source
theorem finset.not_mem_compl {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {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.compl_univ {α : Type u_1} [fintype α] [decidable_eq α] :
finset.univᶜ = ∅
source
@[simp]
theorem finset.compl_eq_empty_iff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
sᶜ = ∅ ↔ s = finset.univ
source
@[simp]
theorem finset.compl_eq_univ_iff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
sᶜ = finset.univ ↔ s = ∅
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 α] {s : finset α} [decidable_eq α] {a : α} :
(s.erase a)ᶜ = has_insert.insert a sᶜ
source
@[simp]
theorem finset.compl_insert {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :
(has_insert.insert a s)ᶜ = sᶜ.erase a
source
@[simp]
theorem finset.insert_compl_self {α : Type u_1} [fintype α] [decidable_eq α] (x : α) :
has_insert.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 : α), has_insert.insert a s) ↑sᶜ
source
theorem finset.image_univ_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq α] [fintype β] {f : β → α} (hf : function.surjective f) :
finset.image f finset.univ = finset.univ
source
theorem finset.map_univ_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : β ↪ α} (hf : function.surjective ⇑f) :
finset.map f finset.univ = finset.univ
source
@[simp]
theorem finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : β ≃ α) :
finset.map f.to_embedding finset.univ = finset.univ
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
@[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
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
@[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
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
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
@[protected, instance]
def finset.decidable_codisjoint {α : Type u_1} [fintype α] [decidable_eq α] {s t : finset α} :
decidable (codisjoint s t)
Equations
source
@[protected, instance]
def finset.decidable_is_compl {α : Type u_1} [fintype α] [decidable_eq α] {s t : finset α} :
decidable (is_compl s t)
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
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
@[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
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
theorem set.to_finset_of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :
p.to_finset = s

Many fintype instances for sets are defined using an extensionally equal finset. Rewriting s.to_finset with set.to_finset_of_finset replaces the term with such a finset.

source
def set.decidable_mem_of_fintype {α : Type u_1} [decidable_eq α] (s : set α) [fintype ↥s] (a : α) :
decidable (a ∈ s)

Membership of a set with a fintype instance is decidable.

Using this as an instance leads to potential loops with subtype.fintype under certain decidability assumptions, so it should only be declared a local instance.

Equations
source
@[simp]
theorem set.coe_to_finset {α : Type u_1} (s : set α) [fintype ↥s] :
↑(s.to_finset) = s
source
@[simp]
theorem set.to_finset_nonempty {α : Type u_1} {s : set α} [fintype ↥s] :
s.to_finset.nonempty ↔ s.nonempty
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
theorem set.to_finset_subset_to_finset {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
s.to_finset ⊆ t.to_finset ↔ s ⊆ t
source
@[simp]
theorem set.to_finset_ssubset {α : Type u_1} {s : set α} [fintype ↥s] {t : finset α} :
s.to_finset ⊂ t ↔ s ⊂ ↑t
source
@[simp]
theorem set.subset_to_finset {α : Type u_1} {t : set α} {s : finset α} [fintype ↥t] :
s ⊆ t.to_finset ↔ ↑s ⊆ t
source
@[simp]
theorem set.ssubset_to_finset {α : Type u_1} {t : set α} {s : finset α} [fintype ↥t] :
s ⊂ t.to_finset ↔ ↑s ⊂ t
source
theorem set.to_finset_ssubset_to_finset {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
s.to_finset ⊂ t.to_finset ↔ s ⊂ t
source
@[simp]
theorem set.to_finset_subset {α : Type u_1} {s : set α} [fintype ↥s] {t : finset α} :
s.to_finset ⊆ t ↔ s ⊆ ↑t
source
theorem set.to_finset_mono {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
s ⊆ t → s.to_finset ⊆ t.to_finset

Alias of the reverse direction of set.to_finset_subset_to_finset.

source
theorem set.to_finset_strict_mono {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
s ⊂ t → s.to_finset ⊂ t.to_finset

Alias of the reverse direction of set.to_finset_ssubset_to_finset.

source
@[simp]
theorem set.disjoint_to_finset {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :
disjoint s.to_finset t.to_finset ↔ disjoint s t
source
@[simp]
theorem set.to_finset_inter {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s ∩ t)] :
(s ∩ t).to_finset = s.to_finset ∩ t.to_finset
source
@[simp]
theorem set.to_finset_union {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s ∪ t)] :
(s ∪ t).to_finset = s.to_finset ∪ t.to_finset
source
@[simp]
theorem set.to_finset_diff {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s \ t)] :
(s \ t).to_finset = s.to_finset \ t.to_finset
source
@[simp]
theorem set.to_finset_symm_diff {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s ∆ t)] :
(s ∆ t).to_finset = s.to_finset ∆ t.to_finset
source
@[simp]
theorem set.to_finset_compl {α : Type u_1} (s : set α) [decidable_eq α] [fintype ↥s] [fintype α] [fintype ↥sᶜ] :
sᶜ.to_finset = s.to_finsetᶜ
source
@[simp]
theorem set.to_finset_empty {α : Type u_1} [fintype ↥∅] :
∅.to_finset = ∅
source
@[simp]
theorem set.to_finset_univ {α : Type u_1} [fintype α] [fintype ↥set.univ] :
set.univ.to_finset = finset.univ
source
@[simp]
theorem set.to_finset_eq_empty {α : Type u_1} {s : set α} [fintype ↥s] :
s.to_finset = ∅ ↔ s = ∅
source
@[simp]
theorem set.to_finset_eq_univ {α : Type u_1} {s : set α} [fintype α] [fintype ↥s] :
s.to_finset = finset.univ ↔ s = set.univ
source
@[simp]
theorem set.to_finset_set_of {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] [fintype ↥{x : α | p x}] :
{x : α | p x}.to_finset = finset.filter p finset.univ
source
@[simp]
theorem set.to_finset_ssubset_univ {α : Type u_1} [fintype α] {s : set α} [fintype ↥s] :
s.to_finset ⊂ finset.univ ↔ s ⊂ set.univ
source
@[simp]
theorem set.to_finset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (s : set α) [fintype ↥s] [fintype ↥(f '' s)] :
(f '' s).to_finset = finset.image f s.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
theorem set.to_finset_singleton {α : Type u_1} (a : α) [fintype ↥{a}] :
{a}.to_finset = {a}
source
@[simp]
theorem set.to_finset_insert {α : Type u_1} [decidable_eq α] {a : α} {s : set α} [fintype ↥(has_insert.insert a s)] [fintype ↥s] :
(has_insert.insert a s).to_finset = has_insert.insert a 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
@[simp]
theorem finset.to_finset_coe {α : Type u_1} (s : finset α) [fintype ↥↑s] :
↑s.to_finset = s
source
@[protected, instance]
def fin.fintype (n : ℕ) :
fintype (fin n)
Equations
source
theorem fin.univ_def (n : ℕ) :
finset.univ = {val := ↑(list.fin_range n), nodup := _}
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 = finset.cons 0 (finset.map {to_fun := fin.succ n, inj' := _} finset.univ) _

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

source
theorem fin.univ_cast_succ (n : ℕ) :
finset.univ = finset.cons (fin.last n) (finset.map fin.cast_succ.to_embedding 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 = finset.cons p (finset.map p.succ_above.to_embedding 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.univ_empty  :
finset.univ = ∅
source
@[simp]
theorem fintype.univ_pempty  :
finset.univ = ∅
source
@[protected, instance]
def unit.fintype  :
fintype unit
Equations
source
theorem fintype.univ_unit  :
finset.univ = {unit.star()}
source
@[protected, instance]
def punit.fintype  :
fintype punit
Equations
source
@[simp]
theorem fintype.univ_punit  :
finset.univ = {punit.star}
source
@[protected, instance]
def bool.fintype  :
fintype bool
Equations
source
@[simp]
theorem fintype.univ_bool  :
finset.univ = {bool.tt, bool.ff}
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
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
@[protected, instance]
def plift.fintype (α : Type u_1) [fintype α] :
fintype (plift α)
Equations
source
@[protected, instance]
def order_dual.fintype (α : Type u_1) [fintype α] :
fintype αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.finite (α : Type u_1) [finite α] :
finite αᵒᵈ
source
@[protected, instance]
def lex.fintype (α : Type u_1) [fintype α] :
fintype (lex α)
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.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
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.univ_Prop  :
finset.univ = {true, false}
source
@[protected, instance]
def subtype.fintype {α : Type u_1} (p : α → Prop) [decidable_pred p] [fintype α] :
fintype {x // p x}
Equations
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
@[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
noncomputable def fintype.finset_equiv_set {α : Type u_1} [fintype α] :
finset α ≃ set α

Given fintype α, finset_equiv_set is the equiv between finset α and set α. (All sets on a finite type are finite.)

Equations
source
@[simp]
theorem fintype.finset_equiv_set_apply {α : Type u_1} [fintype α] (s : finset α) :
⇑fintype.finset_equiv_set s = ↑s
source
@[simp]
theorem fintype.finset_equiv_set_symm_apply {α : Type u_1} [fintype α] (s : set α) [fintype ↥s] :
⇑(fintype.finset_equiv_set.symm) s = s.to_finset
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 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 pfun_fintype (p : Prop) [decidable p] (α : p → Type u_1) [Π (hp : p), fintype (α hp)] :
fintype (Π (hp : p), α hp)
Equations
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 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
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_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
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.