# mathlib3documentation

data.fin_enum

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

Type class for finitely enumerable types. The property is stronger than fintype in that it assigns each element a rank in a finite enumeration.

@[class]
structure fin_enum (α : Sort u_1) :
Sort (max 1 (imax 1 u_1) u_1)

fin_enum α means that α is finite and can be enumerated in some order, i.e. α has an explicit bijection with fin n for some n.

Instances of this typeclass
Instances of other typeclasses for fin_enum
• fin_enum.has_sizeof_inst
def fin_enum.of_equiv (α : Sort u_1) {β : Sort u_2} [fin_enum α] (h : β α) :

transport a fin_enum instance across an equivalence

Equations
def fin_enum.of_nodup_list {α : Type u} [decidable_eq α] (xs : list α) (h : (x : α), x xs) (h' : xs.nodup) :

create a fin_enum instance from an exhaustive list without duplicates

Equations
def fin_enum.of_list {α : Type u} [decidable_eq α] (xs : list α) (h : (x : α), x xs) :

create a fin_enum instance from an exhaustive list; duplicates are removed

Equations
• h = _
def fin_enum.to_list (α : Type u_1) [fin_enum α] :
list α

create an exhaustive list of the values of a given type

Equations
@[simp]
theorem fin_enum.mem_to_list {α : Type u} [fin_enum α] (x : α) :
@[simp]
theorem fin_enum.nodup_to_list {α : Type u} [fin_enum α] :
def fin_enum.of_surjective {α : Type u} {β : Type u_1} (f : β α) [decidable_eq α] [fin_enum β] (h : function.surjective f) :

create a fin_enum instance using a surjection

Equations
• = _
noncomputable def fin_enum.of_injective {α : Type u_1} {β : Type u_2} (f : α β) [decidable_eq α] [fin_enum β] (h : function.injective f) :

create a fin_enum instance using an injection

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def fin_enum.prod {α : Type u} {β : Type u_1} [fin_enum α] [fin_enum β] :
fin_enum × β)
Equations
@[protected, instance]
def fin_enum.sum {α : Type u} {β : Type u_1} [fin_enum α] [fin_enum β] :
fin_enum β)
Equations
@[protected, instance]
def fin_enum.fin {n : } :
Equations
@[protected, instance]
def fin_enum.quotient.enum {α : Type u} [fin_enum α] (s : setoid α)  :
Equations
def fin_enum.finset.enum {α : Type u} [decidable_eq α] :

enumerate all finite sets of a given type

Equations
@[simp]
theorem fin_enum.finset.mem_enum {α : Type u} [decidable_eq α] (s : finset α) (xs : list α) :
(x : α), x s x xs
@[protected, instance]
Equations
@[protected, instance]
def fin_enum.subtype.fin_enum {α : Type u} [fin_enum α] (p : α Prop)  :
fin_enum {x // p x}
Equations
@[protected, instance]
def fin_enum.sigma.fin_enum {α : Type u} (β : α Type v) [fin_enum α] [Π (a : α), fin_enum (β a)] :
Equations
@[protected, instance]
def fin_enum.psigma.fin_enum {α : Type u} {β : α Type v} [fin_enum α] [Π (a : α), fin_enum (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
@[protected, instance]
def fin_enum.psigma.fin_enum_prop_left {α : Prop} {β : α Type v} [Π (a : α), fin_enum (β a)] [decidable α] :
fin_enum (Σ' (a : α), β a)
Equations
@[protected, instance]
def fin_enum.psigma.fin_enum_prop_right {α : Type u} {β : α Prop} [fin_enum α] [Π (a : α), decidable (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
@[protected, instance]
def fin_enum.psigma.fin_enum_prop_prop {α : Prop} {β : α Prop} [decidable α] [Π (a : α), decidable (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
@[protected, instance]
def fin_enum.fintype {α : Type u} [fin_enum α] :
Equations
def fin_enum.pi.cons {α : Type u} {β : α Type v} [decidable_eq α] (x : α) (xs : list α) (y : β x) (f : Π (a : α), a xs β a) (a : α) :
a x :: xs β a

For pi.cons x xs y f create a function where every i ∈ xs is mapped to f i and x is mapped to y

Equations
• xs y f b h = dite (b = x) (λ (h' : b = x), cast _ y) (λ (h' : ¬b = x), f b _)
def fin_enum.pi.tail {α : Type u} {β : α Type v} {x : α} {xs : list α} (f : Π (a : α), a x :: xs β a) (a : α) :
a xs β a

Given f a function whose domain is x :: xs, produce a function whose domain is restricted to xs.

Equations
• h = f a _
def fin_enum.pi {α : Type u} {β : α Type (max u v)} [decidable_eq α] (xs : list α) :
(Π (a : α), list (β a)) list (Π (a : α), a xs β a)

pi xs f creates the list of functions g such that, for x ∈ xs, g x ∈ f x

Equations
theorem fin_enum.mem_pi {α : Type u} {β : α Type (max u v)} [fin_enum α] [Π (a : α), fin_enum (β a)] (xs : list α) (f : Π (a : α), a xs β a) :
f (λ (x : α), fin_enum.to_list (β x))
def fin_enum.pi.enum {α : Type u} (β : α Type (max u v)) [fin_enum α] [Π (a : α), fin_enum (β a)] :
list (Π (a : α), β a)

enumerate all functions whose domain and range are finitely enumerable

Equations
theorem fin_enum.pi.mem_enum {α : Type u} {β : α Type (max u v)} [fin_enum α] [Π (a : α), fin_enum (β a)] (f : Π (a : α), β a) :
@[protected, instance]
def fin_enum.pi.fin_enum {α : Type u} {β : α Type (max u v)} [fin_enum α] [Π (a : α), fin_enum (β a)] :
fin_enum (Π (a : α), β a)
Equations
@[protected, instance]
def fin_enum.pfun_fin_enum (p : Prop) [decidable p] (α : p Type u_1) [Π (hp : p), fin_enum (α hp)] :
fin_enum (Π (hp : p), α hp)
Equations