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 (card α)

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

• decEq : DecidableEq α

@[implicit_reducible]

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

transport a FinEnum instance across an equivalence

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

create an exhaustive list of the values of a given type

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

create a FinEnum instance using a surjection

@[implicit_reducible]

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

@[implicit_reducible]

instance ULift.instFinEnum {α : Type u} [FinEnum α] : FinEnum (ULift.{u_1, u} α)

@[simp]

theorem FinEnum.card_ulift {α : Type u} [FinEnum (ULift.{u_1, u} α)] [FinEnum α] : card (ULift.{u_1, u} α) = card α

@[simp]

theorem FinEnum.equiv_up {α : Type u} [FinEnum α] (a : α) : equiv { down := a } = equiv a

@[simp]

theorem FinEnum.equiv_down {α : Type u} [FinEnum α] (a' : ULift.{u_1, u} α) : equiv a'.down = equiv a'

@[simp]

theorem FinEnum.up_equiv_symm {α : Type u} [FinEnum α] (i : Fin (card α)) : { down := equiv.symm i } = equiv.symm i

@[simp]

theorem FinEnum.down_equiv_symm {α : Type u} [FinEnum α] (i : Fin (card α)) : (equiv.symm i).down = equiv.symm i

@[implicit_reducible]

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

@[implicit_reducible]

instance FinEnum.empty : FinEnum Empty

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

theorem FinEnum.card_fin {n : ℕ} [FinEnum (Fin n)] : card (Fin n) = n

@[implicit_reducible]

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

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

enumerate all finite sets of a given type

@[simp]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance FinEnum.instSubtypeMemListOfDecidableEq {α : Type u} [DecidableEq α] (xs : List α) : FinEnum { x : α // x ∈ xs }

@[implicit_reducible, instance 100]

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

theorem FinEnum.card_eq_fintypeCard {α : Type u} [FinEnum α] [Fintype α] : card α = Fintype.card α

The enumeration merely adds an ordering, leaving the cardinality as is.

theorem FinEnum.card_unique {α : Type u} (e₁ e₂ : FinEnum α) : card α = card α

Any two enumerations of the same type have the same length.

theorem FinEnum.card_eq_zero_iff {α : Type u} [FinEnum α] : card α = 0 ↔ IsEmpty α

A type indexable by Fin 0 is empty and vice versa.

theorem FinEnum.card_eq_zero {α : Type u} [FinEnum α] [IsEmpty α] : card α = 0

Any enumeration of an empty type has length 0.

theorem FinEnum.card_pos_iff {α : Type u} [FinEnum α] : 0 < card α ↔ Nonempty α

A type indexable by Fin n with positive n is inhabited and vice versa.

theorem FinEnum.card_pos {α : Type u_1} [FinEnum α] [Nonempty α] : 0 < card α

Any non-empty enumeration has more than one element.

theorem FinEnum.card_ne_zero {α : Type u_1} [FinEnum α] [Nonempty α] : card α ≠ 0

No non-empty enumeration has 0 elements.

theorem FinEnum.card_eq_one (α : Type u) [FinEnum α] [Unique α] : card α = 1

Any enumeration of a type with unique inhabitant has length 1.

@[implicit_reducible]

instance FinEnum.instUniqueOfIsEmpty {α : Type u} [IsEmpty α] : Unique (FinEnum α)

@[implicit_reducible]

def FinEnum.ofIsEmpty {α : Type u} [IsEmpty α] : FinEnum α

An empty type has a trivial enumeration. Not registered as an instance, to make sure that there aren't two definitionally differing instances around.

@[implicit_reducible]

instance FinEnum.instUnique {α : Type u} [Unique α] : Unique (FinEnum α)

@[implicit_reducible]

def FinEnum.ofUnique {α : Type u} [Unique α] : FinEnum α

A type with unique inhabitant has a trivial enumeration. Not registered as an instance, to make sure that there aren't two definitionally differing instances around.

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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