Mathlib.Data.FinEnum

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

Instances

source

@[implicit_reducible]

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

FinEnum β

transport a FinEnum instance across an equivalence

Equations

FinEnum.ofEquiv α h = { card := FinEnum.card α, equiv := h.trans FinEnum.equiv, decEq := (h.trans FinEnum.equiv).decidableEq }

Instances For

source

@[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

Equations

FinEnum.ofNodupList xs h h' = { card := xs.length, equiv := { toFun := fun (x : α) => ⟨List.idxOf x xs, ⋯⟩, invFun := xs.get, left_inv := ⋯, right_inv := ⋯ }, decEq := inst✝ }

Instances For

source

@[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

Equations

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

Instances For

source

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

card α = xs.dedup.length

source

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

Instances For

source

@[simp]

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

x ∈ toList α

source

@[simp]

theorem FinEnum.nodup_toList {α : Type u} [FinEnum α] :

(toList α).Nodup

source

@[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

Equations

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

Instances For

source

@[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

Equations

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

Instances For

source

@[implicit_reducible]

instance ULift.instFinEnum {α : Type u} [FinEnum α] :

FinEnum (ULift.{u_1, u} α)

Equations

ULift.instFinEnum = { card := FinEnum.card α, equiv := Equiv.ulift.trans FinEnum.equiv, decEq := fun (a b : ULift.{?u.15, ?u.16} α) => instDecidableEqULift a b }

source

@[simp]

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

card (ULift.{u_1, u} α) = card α

source

@[simp]

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

equiv { down := a } = equiv a

source

@[simp]

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

equiv a'.down = equiv a'

source

@[simp]

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

{ down := equiv.symm i } = equiv.symm i

source

@[simp]

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

(equiv.symm i).down = equiv.symm i

source

@[implicit_reducible]

instance FinEnum.pempty :

FinEnum PEmpty.{u_1 + 1}

Equations

FinEnum.pempty = FinEnum.ofList [] FinEnum.pempty._proof_1

source

@[simp]

theorem FinEnum.card_pempty :

card PEmpty.{u_1 + 1} = 0

source

@[implicit_reducible]

instance FinEnum.empty :

FinEnum Empty

Equations

FinEnum.empty = FinEnum.ofList [] FinEnum.empty._proof_1

source

@[simp]

theorem FinEnum.card_empty :

card Empty = 0

source

@[implicit_reducible]

instance FinEnum.punit :

FinEnum PUnit.{u_1 + 1}

Equations

FinEnum.punit = FinEnum.ofList [PUnit.unit ] ⋯

source

@[simp]

theorem FinEnum.card_punit :

card PUnit.{u_1 + 1} = 1

source

@[implicit_reducible]

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

FinEnum (α × β)

Equations

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

source

@[implicit_reducible]

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 β)) ⋯

source

@[implicit_reducible]

instance FinEnum.fin {n : ℕ} :

FinEnum (Fin n)

Equations

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

source

@[simp]

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

card (Fin n) = n

source

@[implicit_reducible]

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

FinEnum (Quotient s)

Equations

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

source

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, insert x_1 r]

Instances For

source

@[simp]

theorem FinEnum.Finset.mem_enum {α : Type u} [DecidableEq α] (s : Finset α) (xs : List α) :

s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs

source

@[implicit_reducible]

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

FinEnum (Finset α)

Equations

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

source

@[implicit_reducible]

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 α)) ⋯

source

@[implicit_reducible]

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

FinEnum (Sigma β)

Equations

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

source

@[implicit_reducible]

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 β)

source

@[implicit_reducible]

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 [] ⋯

source

@[implicit_reducible]

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.

source

@[implicit_reducible]

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 [] ⋯

source

@[implicit_reducible]

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

FinEnum { x : α // x ∈ xs }

Equations

FinEnum.instSubtypeMemListOfDecidableEq xs = FinEnum.ofList xs.attach ⋯

source

@[implicit_reducible, instance 100]

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

Fintype α

Equations

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

source

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

card α = Fintype.card α

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

source

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

card α = card α

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

source

theorem FinEnum.card_eq_zero_iff {α : Type u} [FinEnum α] :

card α = 0 ↔ IsEmpty α

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

source

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

card α = 0

Any enumeration of an empty type has length 0.

source

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.

source

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

0 < card α

Any non-empty enumeration has more than one element.

source

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

card α ≠ 0

No non-empty enumeration has 0 elements.

source

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

card α = 1

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

source

@[implicit_reducible]

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

Unique (FinEnum α)

Equations

FinEnum.instUniqueOfIsEmpty = { default := { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun (a b : α) => decidableEq_of_subsingleton a b }, uniq := ⋯ }

source

@[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.

Equations

FinEnum.ofIsEmpty = default

Instances For

source

@[implicit_reducible]

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

Unique (FinEnum α)

Equations

FinEnum.instUnique = { default := { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun (a b : α) => decidableEq_of_subsingleton a b }, uniq := ⋯ }

source

@[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.

Equations