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

ink

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 : DecidableEq α

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

ink

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

transport a FinEnum instance across an equivalence

Equations

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

ink

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

create a FinEnum instance from an exhaustive list without duplicates

Equations

• One or more equations did not get rendered due to their size.

ink

def FinEnum.ofList {α : Type u} [inst : 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 (List.dedup xs) (_ : ∀ (a : α), a ∈ List.dedup xs) (_ : List.Nodup (List.dedup xs))

ink

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

create an exhaustive list of the values of a given type

Equations

• FinEnum.toList α = List.map (↑(Equiv.symm FinEnum.Equiv)) (List.finRange (FinEnum.card α))

ink

@[simp]

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

ink

@[simp]

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

ink

def FinEnum.ofSurjective {α : Type u} {β : Type u_1} (f : β → α) [inst : DecidableEq α] [inst : 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 β)) (_ : ∀ (x : α), x ∈ List.map f (FinEnum.toList β))

ink

noncomputable def FinEnum.ofInjective {α : Type u_1} {β : Type u_2} (f : α → β) [inst : DecidableEq α] [inst : 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 β)) (_ : ∀ (x : α), x ∈ List.filterMap (Function.partialInv f) (FinEnum.toList β))

ink

instance FinEnum.pempty : FinEnum PEmpty

Equations

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

ink

instance FinEnum.empty : FinEnum Empty

Equations

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

ink

instance FinEnum.punit : FinEnum PUnit

Equations

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

ink

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

Equations

• FinEnum.prod = FinEnum.ofList (FinEnum.toList α ×ˢ FinEnum.toList β) (_ : ∀ (x : α × β), x ∈ FinEnum.toList α ×ˢ FinEnum.toList β)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• FinEnum.fin = FinEnum.ofList (List.finRange n) (_ : ∀ (a : Fin n), a ∈ List.finRange n)

ink

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

Equations

• FinEnum.Quotient.enum s = FinEnum.ofSurjective Quotient.mk'' (_ : ∀ (x : Quotient s), ∃ a, Quotient.mk'' a = x)

ink

def FinEnum.Finset.enum {α : Type u} [inst : 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]

ink

@[simp]

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

ink

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

Equations

• FinEnum.Finset.finEnum = FinEnum.ofList (FinEnum.Finset.enum (FinEnum.toList α)) (_ : ∀ (x : Finset α), x ∈ FinEnum.Finset.enum (FinEnum.toList α))

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

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

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

instance FinEnum.PSigma.finEnumPropProp {α : Prop} {β : α → Prop} [inst : Decidable α] [inst : (a : α) → Decidable (β a)] : FinEnum ((a : α) ×' β a)

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

def FinEnum.Pi.cons {α : Type u} {β : α → Type v} [inst : DecidableEq α] (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

• FinEnum.Pi.cons x xs y f x x = match x, x with | b, h => if h' : b = x then cast (_ : β x = β b) y else f b (_ : b ∈ xs)

ink

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

• FinEnum.Pi.tail f x x = match x, x with | a, h => f a (_ : a ∈ x :: xs)

ink

def FinEnum.pi {α : Type u} {β : α → Type (maxuv)} [inst : DecidableEq α] (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

• FinEnum.pi [] x = [fun x h => False.elim (_ : False)]
• FinEnum.pi (x_2 :: xs) x = Seq.seq (FinEnum.Pi.cons x_2 xs <$> x x_2) fun x => FinEnum.pi xs x

ink

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

ink

def FinEnum.pi.enum {α : Type u} (β : α → Type (maxuv)) [inst : FinEnum α] [inst : (a : α) → FinEnum (β a)] : List ((a : α) → β a)

enumerate all functions whose domain and range are finitely enumerable

Equations

• FinEnum.pi.enum β = List.map (fun f x => f x (_ : x ∈ FinEnum.toList α)) (FinEnum.pi (FinEnum.toList α) fun x => FinEnum.toList (β x))

ink

theorem FinEnum.pi.mem_enum {α : Type u} {β : α → Type (maxuv)} [inst : FinEnum α] [inst : (a : α) → FinEnum (β a)] (f : (a : α) → β a) : f ∈ FinEnum.pi.enum β

ink

instance FinEnum.pi.finEnum {α : Type u} {β : α → Type (maxuv)} [inst : FinEnum α] [inst : (a : α) → FinEnum (β a)] : FinEnum ((a : α) → β a)

Equations

• FinEnum.pi.finEnum = FinEnum.ofList (FinEnum.pi.enum fun a => β a) (_ : ∀ (x : (a : α) → β a), x ∈ FinEnum.pi.enum fun a => β a)

ink

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

Equations

• One or more equations did not get rendered due to their size.