# Documentation

Mathlib.Data.FinEnum

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 FinEnum (α : Sort u_1) :
Sort (max1u_1)
• FinEnum.card is the cardinality of the FinEnum

card :
• FinEnum.Equiv states that type α is in bijection with Fin card, the size of the FinEnum

Equiv : α Fin card
• decEq :

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

Instances
def FinEnum.ofEquiv (α : Sort u_1) {β : Sort u_2} [inst : ] (h : β α) :

transport a FinEnum instance across an equivalence

Equations
def FinEnum.ofNodupList {α : Type u} [inst : ] (xs : List α) (h : ∀ (x : α), x xs) (h' : ) :

create a FinEnum instance from an exhaustive list without duplicates

Equations
• One or more equations did not get rendered due to their size.
def FinEnum.ofList {α : Type u} [inst : ] (xs : List α) (h : ∀ (x : α), x xs) :

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

Equations
def FinEnum.toList (α : Type u_1) [inst : ] :
List α

create an exhaustive list of the values of a given type

Equations
@[simp]
theorem FinEnum.mem_toList {α : Type u} [inst : ] (x : α) :
@[simp]
theorem FinEnum.nodup_toList {α : Type u} [inst : ] :
def FinEnum.ofSurjective {α : Type u} {β : Type u_1} (f : βα) [inst : ] [inst : ] (h : ) :

create a FinEnum instance using a surjection

Equations
noncomputable def FinEnum.ofInjective {α : Type u_1} {β : Type u_2} (f : αβ) [inst : ] [inst : ] (h : ) :

create a FinEnum instance using an injection

Equations
instance FinEnum.pempty :
Equations
instance FinEnum.empty :
Equations
instance FinEnum.punit :
Equations
instance FinEnum.prod {α : Type u} {β : Type u_1} [inst : ] [inst : ] :
FinEnum (α × β)
Equations
instance FinEnum.sum {α : Type u} {β : Type u_1} [inst : ] [inst : ] :
FinEnum (α β)
Equations
• One or more equations did not get rendered due to their size.
instance FinEnum.fin {n : } :
Equations
instance FinEnum.Quotient.enum {α : Type u} [inst : ] (s : ) [inst : DecidableRel fun x x_1 => x x_1] :
Equations
def FinEnum.Finset.enum {α : Type u} [inst : ] :
List αList ()

enumerate all finite sets of a given type

Equations
@[simp]
theorem FinEnum.Finset.mem_enum {α : Type u} [inst : ] (s : ) (xs : List α) :
∀ (x : α), x sx xs
instance FinEnum.Finset.finEnum {α : Type u} [inst : ] :
Equations
instance FinEnum.Subtype.finEnum {α : Type u} [inst : ] (p : αProp) [inst : ] :
FinEnum { x // p x }
Equations
• One or more equations did not get rendered due to their size.
instance FinEnum.instFinEnumSigma {α : Type u} (β : αType v) [inst : ] [inst : (a : α) → FinEnum (β a)] :
Equations
• One or more equations did not get rendered due to their size.
instance FinEnum.PSigma.finEnum {α : Type u} {β : αType v} [inst : ] [inst : (a : α) → FinEnum (β a)] :
FinEnum ((a : α) ×' β a)
Equations
instance FinEnum.PSigma.finEnumPropLeft {α : Prop} {β : αType v} [inst : (a : α) → FinEnum (β a)] [inst : ] :
FinEnum ((a : α) ×' β a)
Equations
• One or more equations did not get rendered due to their size.
instance FinEnum.PSigma.finEnumPropRight {α : Type u} {β : αProp} [inst : ] [inst : (a : α) → Decidable (β a)] :
FinEnum ((a : α) ×' β a)
Equations
• One or more equations did not get rendered due to their size.
instance FinEnum.PSigma.finEnumPropProp {α : Prop} {β : αProp} [inst : ] [inst : (a : α) → Decidable (β a)] :
FinEnum ((a : α) ×' β a)
Equations
• One or more equations did not get rendered due to their size.
instance FinEnum.instFintype {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def FinEnum.Pi.cons {α : Type u} {β : αType v} [inst : ] (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∈ xs is mapped to f i and x is mapped to y

Equations
def FinEnum.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
• = match x, x with | a, h => f a (_ : a x :: xs)
def FinEnum.pi {α : Type u} {β : αType (maxuv)} [inst : ] (xs : List α) :
((a : α) → List (β a)) → List ((a : α) → a xsβ a)

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

Equations
theorem FinEnum.mem_pi {α : Type u} {β : αType (maxuu_1)} [inst : ] [inst : (a : α) → FinEnum (β a)] (xs : List α) (f : (a : α) → a xsβ a) :
f FinEnum.pi xs fun x => FinEnum.toList (β x)
def FinEnum.pi.enum {α : Type u} (β : αType (maxuv)) [inst : ] [inst : (a : α) → FinEnum (β a)] :
List ((a : α) → β a)

enumerate all functions whose domain and range are finitely enumerable

Equations
theorem FinEnum.pi.mem_enum {α : Type u} {β : αType (maxuv)} [inst : ] [inst : (a : α) → FinEnum (β a)] (f : (a : α) → β a) :
instance FinEnum.pi.finEnum {α : Type u} {β : αType (maxuv)} [inst : ] [inst : (a : α) → FinEnum (β a)] :
FinEnum ((a : α) → β a)
Equations
instance FinEnum.pfunFinEnum (p : Prop) [inst : ] (α : pType) [inst : (hp : p) → FinEnum (α hp)] :
FinEnum ((hp : p) → α hp)
Equations
• One or more equations did not get rendered due to their size.