Fintype related definitions and results.

class Fintype (α : Type u) : Type u

Fintype is used to express that a type is finite by requiring a list that contains all elements of this type. (inspired by mathlib)

• elems : List α
• complete (a : α) : a ∈ elems

def subtype_of_list {α : Type u_1} (l : List α) : Type u_1

Subtype of α containing elements of l

Equations

• subtype_of_list l = { x : α // x ∈ l }

instance instFintypeSubtype_of_list {α : Type u_1} {l : List α} : Fintype (subtype_of_list l)

A subtype of α created from the list l is finite.

Equations

• instFintypeSubtype_of_list = { elems := l.attach, complete := ⋯ }

instance instFintypeOption {α : Type u_1} [T : Fintype α] : Fintype (Option α)

If α is finite then Option α is finite as well.

Equations

• instFintypeOption = { elems := List.map (fun (x : α) => some x) Fintype.elems ++ [none], complete := ⋯ }