mathlib documentation

data.fin_enum

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

def fin_enum.of_equiv (α : Sort u_1) {β : Sort u_2} [fin_enum α] :
β αfin_enum β

transport a fin_enum instance across an equivalence

Equations
def fin_enum.of_nodup_list {α : Type u_1} [decidable_eq α] (xs : list α) :
(∀ (x : α), x xs)xs.nodupfin_enum α

create a fin_enum instance from an exhaustive list without duplicates

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

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

Equations
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_1} [fin_enum α] (x : α) :

@[simp]
theorem fin_enum.nodup_to_list {α : Type u_1} [fin_enum α] :

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

create a fin_enum instance using a surjection

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

create a fin_enum instance using an injection

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def fin_enum.prod {α : Type u_1} {β : Type u_2} [fin_enum α] [fin_enum β] :
fin_enum × β)

Equations
@[instance]
def fin_enum.sum {α : Type u_1} {β : Type u_2} [fin_enum α] [fin_enum β] :
fin_enum β)

Equations
@[instance]
def fin_enum.fin {n : } :

Equations
def fin_enum.finset.enum {α : Type u_1} [decidable_eq α] :
list αlist (finset α)

enumerate all finite sets of a given type

Equations
@[simp]
theorem fin_enum.finset.mem_enum {α : Type u_1} [decidable_eq α] (s : finset α) (xs : list α) :
s fin_enum.finset.enum xs ∀ (x : α), x sx xs

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

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

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

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

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

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

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

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

Equations
def fin_enum.pi.cons {α : Type u_1} {β : α → Type u_2} [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
def fin_enum.pi.tail {α : Type u_1} {β : α → Type u_2} {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
def fin_enum.pi {α : Type u_1} {β : α → Type (max u_1 u_2)} [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_1} {β : α → Type (max u_1 u_2)} [fin_enum α] [Π (a : α), fin_enum (β a)] (xs : list α) (f : Π (a : α), a xsβ a) :
f fin_enum.pi xs (λ (x : α), fin_enum.to_list (β x))

def fin_enum.pi.enum {α : Type u_1} (β : α → Type (max u_1 u_2)) [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_1} {β : α → Type (max u_1 u_2)} [fin_enum α] [Π (a : α), fin_enum (β a)] (f : Π (a : α), β a) :

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

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