mathlib3 documentation

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.

source
@[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
source
def fin_enum.of_equiv (α : Sort u_1) {β : Sort u_2} [fin_enum α] (h : β ≃ α) :
fin_enum β

transport a fin_enum instance across an equivalence

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

create a fin_enum instance from an exhaustive list without duplicates

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

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

Equations
source
def fin_enum.to_list (α : Type u_1) [fin_enum α] :
list α

create an exhaustive list of the values of a given type

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

create a fin_enum instance using a surjection

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

create a fin_enum instance using an injection

Equations
source
@[protected, instance]
def fin_enum.pempty  :
fin_enum pempty
Equations
source
@[protected, instance]
def fin_enum.empty  :
fin_enum empty
Equations
source
@[protected, instance]
def fin_enum.punit  :
fin_enum punit
Equations
source
@[protected, instance]
def fin_enum.prod {α : Type u} {β : Type u_1} [fin_enum α] [fin_enum β] :
fin_enum (α × β)
Equations
source
@[protected, instance]
def fin_enum.sum {α : Type u} {β : Type u_1} [fin_enum α] [fin_enum β] :
fin_enum (α ⊕ β)
Equations
source
@[protected, instance]
def fin_enum.fin {n : ℕ} :
fin_enum (fin n)
Equations
source
@[protected, instance]
def fin_enum.quotient.enum {α : Type u} [fin_enum α] (s : setoid α) [decidable_rel has_equiv.equiv] :
fin_enum (quotient s)
Equations
source
def fin_enum.finset.enum {α : Type u} [decidable_eq α] :
list α → list (finset α)

enumerate all finite sets of a given type

Equations
source
@[simp]
theorem fin_enum.finset.mem_enum {α : Type u} [decidable_eq α] (s : finset α) (xs : list α) :
s ∈ fin_enum.finset.enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs
source
@[protected, instance]
def fin_enum.finset.fin_enum {α : Type u} [fin_enum α] :
fin_enum (finset α)
Equations
source
@[protected, instance]
def fin_enum.subtype.fin_enum {α : Type u} [fin_enum α] (p : α → Prop) [decidable_pred p] :
fin_enum {x // p x}
Equations
source
@[protected, instance]
def fin_enum.sigma.fin_enum {α : Type u} (β : α → Type v) [fin_enum α] [Π (a : α), fin_enum (β a)] :
fin_enum (sigma β)
Equations
source
@[protected, instance]
def fin_enum.psigma.fin_enum {α : Type u} {β : α → Type v} [fin_enum α] [Π (a : α), fin_enum (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def fin_enum.psigma.fin_enum_prop_left {α : Prop} {β : α → Type v} [Π (a : α), fin_enum (β a)] [decidable α] :
fin_enum (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def fin_enum.psigma.fin_enum_prop_right {α : Type u} {β : α → Prop} [fin_enum α] [Π (a : α), decidable (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def fin_enum.psigma.fin_enum_prop_prop {α : Prop} {β : α → Prop} [decidable α] [Π (a : α), decidable (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
source
@[protected, instance]
def fin_enum.fintype {α : Type u} [fin_enum α] :
fintype α
Equations
source
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
source
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
source
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
source
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 ∈ fin_enum.pi xs (λ (x : α), fin_enum.to_list (β x))
source
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
source
theorem fin_enum.pi.mem_enum {α : Type u} {β : α → Type (max u v)} [fin_enum α] [Π (a : α), fin_enum (β a)] (f : Π (a : α), β a) :
f ∈ fin_enum.pi.enum β
source
@[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
source
@[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