Documentation

Mathlib.Logic.Equiv.List

Equivalences involving List-like types #

This file defines some additional constructive equivalences using Encodable and the pairing function on .

def Equiv.listEquivOfEquiv {α : Type u_1} {β : Type u_2} (e : α β) :
List α List β

An equivalence between α and β generates an equivalence between List α and List β.

Equations
    Instances For
      def Encodable.encodeList {α : Type u_1} [Encodable α] :
      List α

      Explicit encoding function for List α

      Equations
        Instances For
          @[irreducible]
          def Encodable.decodeList {α : Type u_1} [Encodable α] :
          Option (List α)

          Explicit decoding function for List α

          Equations
            Instances For
              instance List.encodable {α : Type u_1} [Encodable α] :

              If α is encodable, then so is List α. This uses the pair and unpair functions from Data.Nat.Pairing.

              Equations
                instance List.countable {α : Type u_2} [Countable α] :
                @[simp]
                theorem Encodable.encode_list_nil {α : Type u_1} [Encodable α] :
                @[simp]
                theorem Encodable.encode_list_cons {α : Type u_1} [Encodable α] (a : α) (l : List α) :
                encode (a :: l) = (Nat.pair (encode a) (encode l)).succ
                @[simp]
                @[simp]
                theorem Encodable.decode_list_succ {α : Type u_1} [Encodable α] (v : ) :
                decode v.succ = (fun (x1 : α) (x2 : List α) => x1 :: x2) <$> decode (Nat.unpair v).1 <*> decode (Nat.unpair v).2
                theorem Encodable.length_le_encode {α : Type u_1} [Encodable α] (l : List α) :

                These two lemmas are not about lists, but are convenient to keep here and don't require Finset.sort.

                instance Multiset.countable {α : Type u_1} [Countable α] :

                If α is countable, then so is Multiset α.

                instance Finset.countable {α : Type u_1} [Countable α] :

                If α is countable, then so is Finset α.

                def Encodable.encodableOfList {α : Type u_1} [DecidableEq α] (l : List α) (H : ∀ (x : α), x l) :

                A listable type with decidable equality is encodable.

                Equations
                  Instances For

                    A finite type is encodable. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

                    Equations
                      Instances For
                        noncomputable def Fintype.toEncodable (α : Type u_2) [Fintype α] :

                        A noncomputable way to arbitrarily choose an ordering on a finite type. It is not made into a global instance, since it involves an arbitrary choice. This can be locally made into an instance with attribute [local instance] Fintype.toEncodable.

                        Equations
                          Instances For
                            @[irreducible]

                            If α is denumerable, then so is List α.

                            Equations
                              @[simp]
                              theorem Denumerable.list_ofNat_zero {α : Type u_1} [Denumerable α] :
                              ofNat (List α) 0 = []
                              @[simp]
                              theorem Denumerable.list_ofNat_succ {α : Type u_1} [Denumerable α] (v : ) :
                              ofNat (List α) v.succ = ofNat α (Nat.unpair v).1 :: ofNat (List α) (Nat.unpair v).2
                              def Equiv.listUniqueEquiv (α : Type u_1) [Unique α] :

                              A list on a unique type is equivalent to ℕ by sending each list to its length.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem Equiv.listUniqueEquiv_apply (α : Type u_1) [Unique α] (a✝ : List α) :
                                  (listUniqueEquiv α) a✝ = a✝.length
                                  @[deprecated Equiv.listUniqueEquiv (since := "2025-02-17")]

                                  The type lists on unit is canonically equivalent to the natural numbers.

                                  Equations
                                    Instances For

                                      List is equivalent to .

                                      Equations
                                        Instances For
                                          def Equiv.listEquivSelfOfEquivNat {α : Type u_1} (e : α ) :
                                          List α α

                                          If α is equivalent to , then List α is equivalent to α.

                                          Equations
                                            Instances For