Documentation

Mathlib.Data.Fin.Embedding

Embeddings of Fin n #

Fin n is the type whose elements are natural numbers smaller than n. This file defines embeddings between Fin n and other types,

Main definitions #

order #

The inclusion map Fin n → ℕ is an embedding.

Equations
Instances For

    succ and casts into larger Fin types #

    def Fin.succEmb (n : ) :
    Fin n Fin (n + 1)

    Fin.succ as an Embedding

    Equations
    Instances For
      @[simp]
      theorem Fin.coe_succEmb {n : } :
      (succEmb n) = succ
      @[deprecated Fin.coe_succEmb (since := "2025-04-12")]
      theorem Fin.val_succEmb {n : } :
      (succEmb n) = succ

      Alias of Fin.coe_succEmb.

      def Fin.castLEEmb {n m : } (h : n m) :
      Fin n Fin m

      Fin.castLE as an Embedding, castLEEmb h i embeds i into a larger Fin type.

      Equations
      Instances For
        @[simp]
        theorem Fin.castLEEmb_apply {n m : } (h : n m) (i : Fin n) :
        (castLEEmb h) i = castLE h i
        @[simp]
        theorem Fin.coe_castLEEmb {m n : } (hmn : m n) :
        (castLEEmb hmn) = castLE hmn
        theorem Fin.equiv_iff_eq {n m : } :
        Nonempty (Fin m Fin n) m = n
        def Fin.castAddEmb {n : } (m : ) :
        Fin n Fin (n + m)

        Fin.castAdd as an Embedding, castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

        Equations
        Instances For
          @[simp]
          theorem Fin.coe_castAddEmb {n : } (m : ) :
          theorem Fin.castAddEmb_apply {n : } (m : ) (i : Fin n) :
          (castAddEmb m) i = castAdd m i
          def Fin.castSuccEmb {n : } :
          Fin n Fin (n + 1)

          Fin.castSucc as an Embedding, castSuccEmb i embeds i : Fin n in Fin (n+1).

          Equations
          Instances For
            def Fin.addNatEmb {n : } (m : ) :
            Fin n Fin (n + m)

            Fin.addNat as an Embedding, addNatEmb m i adds m to i, generalizes Fin.succ.

            Equations
            Instances For
              @[simp]
              theorem Fin.addNatEmb_apply {n : } (m : ) (x✝ : Fin n) :
              (addNatEmb m) x✝ = x✝.addNat m
              def Fin.natAddEmb (n : ) {m : } :
              Fin m Fin (n + m)

              Fin.natAdd as an Embedding, natAddEmb n i adds n to i "on the left".

              Equations
              Instances For
                @[simp]
                theorem Fin.natAddEmb_apply (n : ) {m : } (i : Fin m) :
                (natAddEmb n) i = natAdd n i
                def Fin.succAboveEmb {n : } (p : Fin (n + 1)) :
                Fin n Fin (n + 1)

                Fin.succAbove p as an Embedding.

                Equations
                Instances For
                  @[simp]
                  theorem Fin.succAboveEmb_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
                  @[simp]
                  theorem Fin.coe_succAboveEmb {n : } (p : Fin (n + 1)) :