Documentation

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.

class FinEnum (α : Sort u_1) :
Sort (max1u_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.

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

    transport a FinEnum instance across an equivalence

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

    create a FinEnum instance from an exhaustive list without duplicates

    Equations
    • One or more equations did not get rendered due to their size.
    def FinEnum.ofList {α : Type u} [inst : DecidableEq α] (xs : List α) (h : ∀ (x : α), x xs) :

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

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

    create an exhaustive list of the values of a given type

    Equations
    @[simp]
    theorem FinEnum.mem_toList {α : Type u} [inst : FinEnum α] (x : α) :
    @[simp]
    theorem FinEnum.nodup_toList {α : Type u} [inst : FinEnum α] :
    def FinEnum.ofSurjective {α : Type u} {β : Type u_1} (f : βα) [inst : DecidableEq α] [inst : FinEnum β] (h : Function.Surjective f) :

    create a FinEnum instance using a surjection

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

    create a FinEnum instance using an injection

    Equations
    instance FinEnum.prod {α : Type u} {β : Type u_1} [inst : FinEnum α] [inst : FinEnum β] :
    FinEnum (α × β)
    Equations
    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.
    instance FinEnum.fin {n : } :
    Equations
    instance FinEnum.Quotient.enum {α : Type u} [inst : FinEnum α] (s : Setoid α) [inst : DecidableRel fun x x_1 => x x_1] :
    Equations
    def FinEnum.Finset.enum {α : Type u} [inst : DecidableEq α] :
    List αList (Finset α)

    enumerate all finite sets of a given type

    Equations
    @[simp]
    theorem FinEnum.Finset.mem_enum {α : Type u} [inst : DecidableEq α] (s : Finset α) (xs : List α) :
    s FinEnum.Finset.enum xs ∀ (x : α), x sx xs
    instance FinEnum.Finset.finEnum {α : Type u} [inst : FinEnum α] :
    Equations
    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.
    instance FinEnum.instFinEnumSigma {α : Type u} (β : αType v) [inst : FinEnum α] [inst : (a : α) → FinEnum (β a)] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance FinEnum.PSigma.finEnum {α : Type u} {β : αType v} [inst : FinEnum α] [inst : (a : α) → FinEnum (β a)] :
    FinEnum ((a : α) ×' β a)
    Equations
    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.
    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.
    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.
    instance FinEnum.instFintype {α : Type u} [inst : FinEnum α] :
    Equations
    • One or more equations did not get rendered due to their size.
    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
    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
    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
    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)
    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
    theorem FinEnum.pi.mem_enum {α : Type u} {β : αType (maxuv)} [inst : FinEnum α] [inst : (a : α) → FinEnum (β a)] (f : (a : α) → β a) :
    instance FinEnum.pi.finEnum {α : Type u} {β : αType (maxuv)} [inst : FinEnum α] [inst : (a : α) → FinEnum (β a)] :
    FinEnum ((a : α) → β a)
    Equations
    instance FinEnum.pfunFinEnum (p : Prop) [inst : Decidable p] (α : pType) [inst : (hp : p) → FinEnum (α hp)] :
    FinEnum ((hp : p) → α hp)
    Equations
    • One or more equations did not get rendered due to their size.