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 (max 1 u_1)

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

• card : ℕ

  FinEnum.card is the cardinality of the FinEnum

• equiv : α ≃ Fin (FinEnum.card α)

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

• decEq : DecidableEq α

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

transport a FinEnum instance across an equivalence

Equations

• FinEnum.ofEquiv α h = FinEnum.mk (FinEnum.card α) (h.trans FinEnum.equiv)

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

create a FinEnum instance from an exhaustive list without duplicates

Equations

• FinEnum.ofNodupList xs h h' = FinEnum.mk xs.length { toFun := fun (x : α) => ⟨List.indexOf x xs, ⋯⟩, invFun := xs.get, left_inv := ⋯, right_inv := ⋯ }

def FinEnum.ofList {α : Type u} [DecidableEq α] (xs : List α) (h : ∀ (x : α), x ∈ xs) : FinEnum α

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

Equations

• FinEnum.ofList xs h = FinEnum.ofNodupList xs.dedup ⋯ ⋯

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

create an exhaustive list of the values of a given type

Equations

• FinEnum.toList α = List.map (⇑FinEnum.equiv.symm) (List.finRange (FinEnum.card α))

@[simp]

theorem FinEnum.mem_toList {α : Type u} [FinEnum α] (x : α) : x ∈ FinEnum.toList α

@[simp]

theorem FinEnum.nodup_toList {α : Type u} [FinEnum α] : (FinEnum.toList α).Nodup

def FinEnum.ofSurjective {α : Type u} {β : Type u_1} (f : β → α) [DecidableEq α] [FinEnum β] (h : Function.Surjective f) : FinEnum α

create a FinEnum instance using a surjection

Equations

• FinEnum.ofSurjective f h = FinEnum.ofList (List.map f (FinEnum.toList β)) ⋯

noncomputable def FinEnum.ofInjective {α : Type u_1} {β : Type u_2} (f : α → β) [DecidableEq α] [FinEnum β] (h : Function.Injective f) : FinEnum α

create a FinEnum instance using an injection

Equations

• FinEnum.ofInjective f h = FinEnum.ofList (List.filterMap (Function.partialInv f) (FinEnum.toList β)) ⋯

instance FinEnum.pempty : FinEnum PEmpty.{u_1 + 1}

Equations

• FinEnum.pempty = FinEnum.ofList [] FinEnum.pempty.proof_1

instance FinEnum.empty : FinEnum Empty

Equations

• FinEnum.empty = FinEnum.ofList [] FinEnum.empty.proof_1

instance FinEnum.punit : FinEnum PUnit.{u_1 + 1}

Equations

• FinEnum.punit = FinEnum.ofList [PUnit.unit] FinEnum.punit.proof_1

instance FinEnum.prod {α : Type u} {β : Type u_1} [FinEnum α] [FinEnum β] : FinEnum (α × β)

Equations

• FinEnum.prod = FinEnum.ofList (FinEnum.toList α ×ˢ FinEnum.toList β) ⋯

instance FinEnum.sum {α : Type u} {β : Type u_1} [FinEnum α] [FinEnum β] : FinEnum (α ⊕ β)

Equations

• FinEnum.sum = FinEnum.ofList (List.map Sum.inl (FinEnum.toList α) ++ List.map Sum.inr (FinEnum.toList β)) ⋯

instance FinEnum.fin {n : ℕ} : FinEnum (Fin n)

Equations

• FinEnum.fin = FinEnum.ofList (List.finRange n) ⋯

instance FinEnum.Quotient.enum {α : Type u} [FinEnum α] (s : Setoid α) [DecidableRel fun (x x_1 : α) => x ≈ x_1] : FinEnum (Quotient s)

Equations

• FinEnum.Quotient.enum s = FinEnum.ofSurjective Quotient.mk'' ⋯

def FinEnum.Finset.enum {α : Type u} [DecidableEq α] : List α → List (Finset α)

enumerate all finite sets of a given type

Equations

• FinEnum.Finset.enum [] = [∅]
• FinEnum.Finset.enum (x_1 :: xs) = do let r ← FinEnum.Finset.enum xs [r, {x_1} ∪ r]

@[simp]

theorem FinEnum.Finset.mem_enum {α : Type u} [DecidableEq α] (s : Finset α) (xs : List α) : s ∈ FinEnum.Finset.enum xs ↔ ∀ x ∈ s, x ∈ xs

instance FinEnum.Finset.finEnum {α : Type u} [FinEnum α] : FinEnum (Finset α)

Equations

• FinEnum.Finset.finEnum = FinEnum.ofList (FinEnum.Finset.enum (FinEnum.toList α)) ⋯

instance FinEnum.Subtype.finEnum {α : Type u} [FinEnum α] (p : α → Prop) [DecidablePred p] : FinEnum { x : α // p x }

Equations

• FinEnum.Subtype.finEnum p = FinEnum.ofList (List.filterMap (fun (x : α) => if h : p x then some ⟨x, h⟩ else none) (FinEnum.toList α)) ⋯

instance FinEnum.instSigma {α : Type u} (β : α → Type v) [FinEnum α] [(a : α) → FinEnum (β a)] : FinEnum (Sigma β)

Equations

• FinEnum.instSigma β = FinEnum.ofList ((FinEnum.toList α).bind fun (a : α) => List.map (Sigma.mk a) (FinEnum.toList (β a))) ⋯

instance FinEnum.PSigma.finEnum {α : Type u} {β : α → Type v} [FinEnum α] [(a : α) → FinEnum (β a)] : FinEnum ((a : α) ×' β a)

Equations

• FinEnum.PSigma.finEnum = FinEnum.ofEquiv ((i : α) × β i) (Equiv.psigmaEquivSigma β)

instance FinEnum.PSigma.finEnumPropLeft {α : Prop} {β : α → Type v} [(a : α) → FinEnum (β a)] [Decidable α] : FinEnum ((a : α) ×' β a)

Equations

• FinEnum.PSigma.finEnumPropLeft = if h : α then FinEnum.ofList (List.map (PSigma.mk h) (FinEnum.toList (β h))) ⋯ else FinEnum.ofList [] ⋯

instance FinEnum.PSigma.finEnumPropRight {α : Type u} {β : α → Prop} [FinEnum α] [(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} [Decidable α] [(a : α) → Decidable (β a)] : FinEnum ((a : α) ×' β a)

Equations

• FinEnum.PSigma.finEnumPropProp = if h : ∃ (a : α), β a then FinEnum.ofList [⟨⋯, ⋯⟩] ⋯ else FinEnum.ofList [] ⋯

@[instance 100]

instance FinEnum.instFintype {α : Type u} [FinEnum α] : Fintype α

Equations

• FinEnum.instFintype = { elems := Finset.map FinEnum.equiv.symm.toEmbedding Finset.univ, complete := ⋯ }

theorem List.mem_pi_toList {α : Type u_1} [FinEnum α] {β : α → Type u_2} [(a : α) → FinEnum (β a)] (xs : List α) (f : (a : α) → a ∈ xs → β a) : f ∈ xs.pi fun (x : α) => FinEnum.toList (β x)

def List.Pi.enum {α : Type u_1} [FinEnum α] (β : α → Type u_3) [(a : α) → FinEnum (β a)] : List ((a : α) → β a)

enumerate all functions whose domain and range are finitely enumerable

Equations

• List.Pi.enum β = List.map (fun (f : (i : α) → i ∈ FinEnum.toList α → β i) (x : α) => f x ⋯) ((FinEnum.toList α).pi fun (x : α) => FinEnum.toList (β x))

theorem List.Pi.mem_enum {α : Type u_1} [FinEnum α] {β : α → Type u_2} [(a : α) → FinEnum (β a)] (f : (a : α) → β a) : f ∈ List.Pi.enum β

instance List.Pi.finEnum {α : Type u_1} [FinEnum α] {β : α → Type u_2} [(a : α) → FinEnum (β a)] : FinEnum ((a : α) → β a)

Equations

• List.Pi.finEnum = FinEnum.ofList (List.Pi.enum β) ⋯

instance List.pfunFinEnum (p : Prop) [Decidable p] (α : p → Type) [(hp : p) → FinEnum (α hp)] : FinEnum ((hp : p) → α hp)

Equations

• List.pfunFinEnum p α = if hp : p then FinEnum.ofList (List.map (fun (x : α hp) (x_1 : p) => x) (FinEnum.toList (α hp))) ⋯ else FinEnum.ofList [fun (hp' : p) => ⋯.elim] ⋯