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 (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.

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

    transport a FinEnum instance across an equivalence

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

      create a FinEnum instance from an exhaustive list without duplicates

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

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

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

          create an exhaustive list of the values of a given type

          Equations
          Instances For
            @[simp]
            theorem FinEnum.mem_toList {α : Type u} [FinEnum α] (x : α) :
            @[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) :

            create a FinEnum instance using a surjection

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

              create a FinEnum instance using an injection

              Equations
              Instances For
                instance FinEnum.prod {α : Type u} {β : Type u_1} [FinEnum α] [FinEnum β] :
                FinEnum (α × β)
                Equations
                instance FinEnum.sum {α : Type u} {β : Type u_1} [FinEnum α] [FinEnum β] :
                FinEnum (α β)
                Equations
                instance FinEnum.fin {n : } :
                Equations
                instance FinEnum.Quotient.enum {α : Type u} [FinEnum α] (s : Setoid α) [DecidableRel fun (x x_1 : α) => x x_1] :
                Equations
                def FinEnum.Finset.enum {α : Type u} [DecidableEq α] :
                List αList (Finset α)

                enumerate all finite sets of a given type

                Equations
                Instances For
                  @[simp]
                  theorem FinEnum.Finset.mem_enum {α : Type u} [DecidableEq α] (s : Finset α) (xs : List α) :
                  s FinEnum.Finset.enum xs xs, x xs
                  instance FinEnum.Finset.finEnum {α : Type u} [FinEnum α] :
                  Equations
                  instance FinEnum.Subtype.finEnum {α : Type u} [FinEnum α] (p : αProp) [DecidablePred p] :
                  FinEnum { x : α // p x }
                  Equations
                  instance FinEnum.instSigma {α : Type u} (β : αType v) [FinEnum α] [(a : α) → FinEnum (β a)] :
                  Equations
                  instance FinEnum.PSigma.finEnum {α : Type u} {β : αType v} [FinEnum α] [(a : α) → FinEnum (β a)] :
                  FinEnum ((a : α) ×' β a)
                  Equations
                  instance FinEnum.PSigma.finEnumPropLeft {α : Prop} {β : αType v} [(a : α) → FinEnum (β a)] [Decidable α] :
                  FinEnum ((a : α) ×' β a)
                  Equations
                  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
                  @[instance 100]
                  instance FinEnum.instFintype {α : Type u} [FinEnum α] :
                  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
                  Instances For
                    theorem List.Pi.mem_enum {α : Type u_1} [FinEnum α] {β : αType u_2} [(a : α) → FinEnum (β a)] (f : (a : α) → β a) :
                    instance List.Pi.finEnum {α : Type u_1} [FinEnum α] {β : αType u_2} [(a : α) → FinEnum (β a)] :
                    FinEnum ((a : α) → β a)
                    Equations
                    instance List.pfunFinEnum (p : Prop) [Decidable p] (α : pType) [(hp : p) → FinEnum (α hp)] :
                    FinEnum ((hp : p) → α hp)
                    Equations