Documentation

Mathlib.Logic.Equiv.Fin

Equivalences for Fin n #

Equivalence between Fin 0 and Empty.

Equations
Instances For

    Equivalence between Fin 0 and PEmpty.

    Equations
    Instances For

      Equivalence between Fin 1 and Unit.

      Equations
      Instances For

        Equivalence between Fin 2 and Bool.

        Equations
        Instances For

          Tuples #

          This section defines a bunch of equivalences between n + 1-tuples and products of n-tuples with an entry.

          @[simp]
          theorem Fin.consEquiv_symm_apply {n : } (α : Fin (n + 1)Type u_1) (f : (i : Fin (n + 1)) → α i) :
          (Fin.consEquiv α).symm f = (f 0, Fin.tail f)
          @[simp]
          theorem Fin.consEquiv_apply {n : } (α : Fin (n + 1)Type u_1) (f : α 0 × ((i : Fin n) → α i.succ)) (i : Fin (n + 1)) :
          (Fin.consEquiv α) f i = Fin.cons f.1 f.2 i
          def Fin.consEquiv {n : } (α : Fin (n + 1)Type u_1) :
          α 0 × ((i : Fin n) → α i.succ) ((i : Fin (n + 1)) → α i)

          Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the first element of the tuple.

          This is Fin.cons as an Equiv.

          Equations
          • Fin.consEquiv α = { toFun := fun (f : α 0 × ((i : Fin n) → α i.succ)) => Fin.cons f.1 f.2, invFun := fun (f : (i : Fin (n + 1)) → α i) => (f 0, Fin.tail f), left_inv := , right_inv := }
          Instances For
            @[simp]
            theorem Fin.snocEquiv_apply {n : } (α : Fin (n + 1)Type u_1) (f : α (Fin.last n) × ((i : Fin n) → α i.castSucc)) :
            ∀ (x : Fin (n + 1)), (Fin.snocEquiv α) f x = Fin.snoc f.2 f.1 x
            @[simp]
            theorem Fin.snocEquiv_symm_apply {n : } (α : Fin (n + 1)Type u_1) (f : (i : Fin (n + 1)) → α i) :
            (Fin.snocEquiv α).symm f = (f (Fin.last n), Fin.init f)
            def Fin.snocEquiv {n : } (α : Fin (n + 1)Type u_1) :
            α (Fin.last n) × ((i : Fin n) → α i.castSucc) ((i : Fin (n + 1)) → α i)

            Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the last element of the tuple.

            This is Fin.snoc as an Equiv.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Fin.insertNthEquiv_symm_apply {n : } (α : Fin (n + 1)Type u) (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) :
              (Fin.insertNthEquiv α p).symm f = (f p, p.removeNth f)
              @[simp]
              theorem Fin.insertNthEquiv_apply {n : } (α : Fin (n + 1)Type u) (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)) :
              (Fin.insertNthEquiv α p) f j = p.insertNth f.1 f.2 j
              def Fin.insertNthEquiv {n : } (α : Fin (n + 1)Type u) (p : Fin (n + 1)) :
              α p × ((i : Fin n) → α (p.succAbove i)) ((i : Fin (n + 1)) → α i)

              Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the p-th element of the tuple.

              This is Fin.insertNth as an Equiv.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Fin.insertNthEquiv_zero {n : } (α : Fin (n + 1)Type u_1) :
                @[simp]
                theorem Fin.insertNthEquiv_last (n : ) (α : Type u_1) :
                Fin.insertNthEquiv (fun (x : Fin (n + 1)) => α) (Fin.last n) = Fin.snocEquiv fun (x : Fin (n + 1)) => α

                Note this lemma can only be written about non-dependent tuples as insertNth (last n) = snoc is not a definitional equality.

                @[simp]
                theorem piFinTwoEquiv_apply (α : Fin 2Type u) :
                (piFinTwoEquiv α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)
                @[simp]
                theorem piFinTwoEquiv_symm_apply (α : Fin 2Type u) :
                (piFinTwoEquiv α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                def piFinTwoEquiv (α : Fin 2Type u) :
                ((i : Fin 2) → α i) α 0 × α 1

                Π i : Fin 2, α i is equivalent to α 0 × α 1. See also finTwoArrowEquiv for a non-dependent version and prodEquivPiFinTwo for a version with inputs α β : Type u.

                Equations
                • piFinTwoEquiv α = { toFun := fun (f : (i : Fin 2) → α i) => (f 0, f 1), invFun := fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim), left_inv := , right_inv := }
                Instances For

                  Miscellaneous #

                  This is currently not very sorted. PRs welcome!

                  theorem Fin.preimage_apply_01_prod {α : Fin 2Type u} (s : Set (α 0)) (t : Set (α 1)) :
                  (fun (f : (i : Fin 2) → α i) => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi (Fin.cons s (Fin.cons t finZeroElim))
                  theorem Fin.preimage_apply_01_prod' {α : Type u} (s : Set α) (t : Set α) :
                  (fun (f : Fin 2α) => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi ![s, t]
                  @[simp]
                  theorem prodEquivPiFinTwo_apply (α : Type u) (β : Type u) :
                  (prodEquivPiFinTwo α β) = fun (p : Fin.cons α (Fin.cons β finZeroElim) 0 × Fin.cons α (Fin.cons β finZeroElim) 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                  @[simp]
                  theorem prodEquivPiFinTwo_symm_apply (α : Type u) (β : Type u) :
                  (prodEquivPiFinTwo α β).symm = fun (f : (i : Fin 2) → Fin.cons α (Fin.cons β finZeroElim) i) => (f 0, f 1)
                  def prodEquivPiFinTwo (α : Type u) (β : Type u) :
                  α × β ((i : Fin 2) → ![α, β] i)

                  A product space α × β is equivalent to the space Π i : Fin 2, γ i, where γ = Fin.cons α (Fin.cons β finZeroElim). See also piFinTwoEquiv and finTwoArrowEquiv.

                  Equations
                  Instances For
                    @[simp]
                    theorem finTwoArrowEquiv_apply (α : Type u_1) :
                    (finTwoArrowEquiv α) = (piFinTwoEquiv fun (x : Fin 2) => α).toFun
                    @[simp]
                    theorem finTwoArrowEquiv_symm_apply (α : Type u_1) :
                    (finTwoArrowEquiv α).symm = fun (x : α × α) => ![x.1, x.2]
                    def finTwoArrowEquiv (α : Type u_1) :
                    (Fin 2α) α × α

                    The space of functions Fin 2 → α is equivalent to α × α. See also piFinTwoEquiv and prodEquivPiFinTwo.

                    Equations
                    Instances For
                      def finSuccEquiv' {n : } (i : Fin (n + 1)) :
                      Fin (n + 1) Option (Fin n)

                      An equivalence that removes i and maps it to none. This is a version of Fin.predAbove that produces Option (Fin n) instead of mapping both i.cast_succ and i.succ to i.

                      Equations
                      • finSuccEquiv' i = { toFun := i.insertNth none some, invFun := fun (x : Option (Fin n)) => x.casesOn' i i.succAbove, left_inv := , right_inv := }
                      Instances For
                        @[simp]
                        theorem finSuccEquiv'_at {n : } (i : Fin (n + 1)) :
                        (finSuccEquiv' i) i = none
                        @[simp]
                        theorem finSuccEquiv'_succAbove {n : } (i : Fin (n + 1)) (j : Fin n) :
                        (finSuccEquiv' i) (i.succAbove j) = some j
                        theorem finSuccEquiv'_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
                        (finSuccEquiv' i) m.castSucc = some m
                        theorem finSuccEquiv'_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
                        (finSuccEquiv' i) m.succ = some m
                        @[simp]
                        theorem finSuccEquiv'_symm_none {n : } (i : Fin (n + 1)) :
                        (finSuccEquiv' i).symm none = i
                        @[simp]
                        theorem finSuccEquiv'_symm_some {n : } (i : Fin (n + 1)) (j : Fin n) :
                        (finSuccEquiv' i).symm (some j) = i.succAbove j
                        theorem finSuccEquiv'_symm_some_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
                        (finSuccEquiv' i).symm (some m) = m.castSucc
                        theorem finSuccEquiv'_symm_some_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
                        (finSuccEquiv' i).symm (some m) = m.succ
                        theorem finSuccEquiv'_symm_coe_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
                        (finSuccEquiv' i).symm (some m) = m.castSucc
                        theorem finSuccEquiv'_symm_coe_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
                        (finSuccEquiv' i).symm (some m) = m.succ
                        def finSuccEquiv (n : ) :
                        Fin (n + 1) Option (Fin n)

                        Equivalence between Fin (n + 1) and Option (Fin n). This is a version of Fin.pred that produces Option (Fin n) instead of requiring a proof that the input is not 0.

                        Equations
                        Instances For
                          @[simp]
                          theorem finSuccEquiv_zero {n : } :
                          (finSuccEquiv n) 0 = none
                          @[simp]
                          theorem finSuccEquiv_succ {n : } (m : Fin n) :
                          (finSuccEquiv n) m.succ = some m
                          @[simp]
                          theorem finSuccEquiv_symm_none {n : } :
                          (finSuccEquiv n).symm none = 0
                          @[simp]
                          theorem finSuccEquiv_symm_some {n : } (m : Fin n) :
                          (finSuccEquiv n).symm (some m) = m.succ
                          theorem finSuccEquiv'_last_apply_castSucc {n : } (i : Fin n) :
                          (finSuccEquiv' (Fin.last n)) i.castSucc = some i
                          theorem finSuccEquiv'_last_apply {n : } {i : Fin (n + 1)} (h : i Fin.last n) :
                          (finSuccEquiv' (Fin.last n)) i = some (i.castLT )
                          theorem finSuccEquiv'_ne_last_apply {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (hi : i Fin.last n) (hj : j i) :
                          (finSuccEquiv' i) j = some ((i.castLT ).predAbove j)
                          def finSuccAboveEquiv {n : } (p : Fin (n + 1)) :
                          Fin n { x : Fin (n + 1) // x p }

                          Fin.succAbove as an order isomorphism between Fin n and {x : Fin (n + 1) // x ≠ p}.

                          Equations
                          Instances For
                            theorem finSuccAboveEquiv_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
                            (finSuccAboveEquiv p) i = p.succAbove i,
                            theorem finSuccAboveEquiv_symm_apply_last {n : } (x : { x : Fin (n + 1) // x Fin.last n }) :
                            (finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT
                            theorem finSuccAboveEquiv_symm_apply_ne_last {n : } {p : Fin (n + 1)} (h : p Fin.last n) (x : { x : Fin (n + 1) // x p }) :
                            (finSuccAboveEquiv p).symm x = (p.castLT ).predAbove x
                            def finSuccEquivLast {n : } :
                            Fin (n + 1) Option (Fin n)

                            Equiv between Fin (n + 1) and Option (Fin n) sending Fin.last n to none

                            Equations
                            Instances For
                              @[simp]
                              theorem finSuccEquivLast_castSucc {n : } (i : Fin n) :
                              finSuccEquivLast i.castSucc = some i
                              @[simp]
                              theorem finSuccEquivLast_last {n : } :
                              finSuccEquivLast (Fin.last n) = none
                              @[simp]
                              theorem finSuccEquivLast_symm_some {n : } (i : Fin n) :
                              finSuccEquivLast.symm (some i) = i.castSucc
                              @[simp]
                              theorem finSuccEquivLast_symm_none {n : } :
                              finSuccEquivLast.symm none = Fin.last n
                              @[simp]
                              theorem Equiv.piFinSuccAbove_apply {n : } (α : Fin (n + 1)Type u) (i : Fin (n + 1)) :
                              (Equiv.piFinSuccAbove α i) = fun (f : (j : Fin (n + 1)) → α j) => (f i, i.removeNth f)
                              @[simp]
                              theorem Equiv.piFinSuccAbove_symm_apply {n : } (α : Fin (n + 1)Type u) (i : Fin (n + 1)) :
                              (Equiv.piFinSuccAbove α i).symm = fun (f : α i × ((j : Fin n) → α (i.succAbove j))) => i.insertNth f.1 f.2
                              @[deprecated Fin.insertNthEquiv]
                              def Equiv.piFinSuccAbove {n : } (α : Fin (n + 1)Type u) (i : Fin (n + 1)) :
                              ((j : Fin (n + 1)) → α j) α i × ((j : Fin n) → α (i.succAbove j))

                              Equivalence between Π j : Fin (n + 1), α j and α i × Π j : Fin n, α (Fin.succAbove i j).

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem Equiv.piFinSucc_symm_apply (n : ) (β : Type u) :
                                (Equiv.piFinSucc n β).symm = (Fin.consEquiv fun (x : Fin (n + 1)) => β)
                                @[simp]
                                theorem Equiv.piFinSucc_apply (n : ) (β : Type u) :
                                (Equiv.piFinSucc n β) = (Fin.consEquiv fun (x : Fin (n + 1)) => β).symm
                                @[deprecated Fin.consEquiv]
                                def Equiv.piFinSucc (n : ) (β : Type u) :
                                (Fin (n + 1)β) β × (Fin nβ)

                                Equivalence between Fin (n + 1) → β and β × (Fin n → β).

                                Equations
                                Instances For
                                  def Equiv.embeddingFinSucc (n : ) (ι : Type u_1) :
                                  (Fin (n + 1) ι) (e : Fin n ι) × { i : ι // iSet.range e }

                                  An embedding e : Fin (n+1) ↪ ι corresponds to an embedding f : Fin n ↪ ι (corresponding the last n coordinates of e) together with a value not taken by f (corresponding to e 0).

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Equiv.embeddingFinSucc_fst {n : } {ι : Type u_1} (e : Fin (n + 1) ι) :
                                    ((Equiv.embeddingFinSucc n ι) e).fst = e Fin.succ
                                    @[simp]
                                    theorem Equiv.embeddingFinSucc_snd {n : } {ι : Type u_1} (e : Fin (n + 1) ι) :
                                    ((Equiv.embeddingFinSucc n ι) e).snd = e 0
                                    @[simp]
                                    theorem Equiv.coe_embeddingFinSucc_symm {n : } {ι : Type u_1} (f : (e : Fin n ι) × { i : ι // iSet.range e }) :
                                    ((Equiv.embeddingFinSucc n ι).symm f) = Fin.cons f.snd f.fst
                                    @[simp]
                                    theorem Equiv.piFinCastSucc_apply (n : ) (β : Type u) :
                                    (Equiv.piFinCastSucc n β) = (Fin.snocEquiv fun (x : Fin (n + 1)) => β).symm
                                    @[simp]
                                    theorem Equiv.piFinCastSucc_symm_apply (n : ) (β : Type u) :
                                    (Equiv.piFinCastSucc n β).symm = (Fin.snocEquiv fun (x : Fin (n + 1)) => β)
                                    @[deprecated Fin.snocEquiv]
                                    def Equiv.piFinCastSucc (n : ) (β : Type u) :
                                    (Fin (n + 1)β) β × (Fin nβ)

                                    Equivalence between Fin (n + 1) → β and β × (Fin n → β) which separates out the last element of the tuple.

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

                                      Equivalence between Fin m ⊕ Fin n and Fin (m + n)

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem finSumFinEquiv_apply_left {m : } {n : } (i : Fin m) :
                                        finSumFinEquiv (Sum.inl i) = Fin.castAdd n i
                                        @[simp]
                                        theorem finSumFinEquiv_apply_right {m : } {n : } (i : Fin n) :
                                        finSumFinEquiv (Sum.inr i) = Fin.natAdd m i
                                        @[simp]
                                        theorem finSumFinEquiv_symm_apply_castAdd {m : } {n : } (x : Fin m) :
                                        finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x
                                        @[simp]
                                        theorem finSumFinEquiv_symm_apply_natAdd {m : } {n : } (x : Fin n) :
                                        finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x
                                        @[simp]
                                        theorem finSumFinEquiv_symm_last {n : } :
                                        finSumFinEquiv.symm (Fin.last n) = Sum.inr 0
                                        def finAddFlip {m : } {n : } :
                                        Fin (m + n) Fin (n + m)

                                        The equivalence between Fin (m + n) and Fin (n + m) which rotates by n.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem finAddFlip_apply_castAdd {m : } (k : Fin m) (n : ) :
                                          finAddFlip (Fin.castAdd n k) = Fin.natAdd n k
                                          @[simp]
                                          theorem finAddFlip_apply_natAdd {n : } (k : Fin n) (m : ) :
                                          finAddFlip (Fin.natAdd m k) = Fin.castAdd m k
                                          @[simp]
                                          theorem finAddFlip_apply_mk_left {m : } {n : } {k : } (h : k < m) (hk : optParam (k < m + n) ) (hnk : optParam (n + k < n + m) ) :
                                          finAddFlip k, hk = n + k, hnk
                                          @[simp]
                                          theorem finAddFlip_apply_mk_right {m : } {n : } {k : } (h₁ : m k) (h₂ : k < m + n) :
                                          finAddFlip k, h₂ = k - m,
                                          def finRotate (n : ) :

                                          Rotate Fin n one step to the right.

                                          Equations
                                          Instances For
                                            theorem finRotate_succ (n : ) :
                                            finRotate (n + 1) = finAddFlip.trans (finCongr )
                                            theorem finRotate_of_lt {n : } {k : } (h : k < n) :
                                            (finRotate (n + 1)) k, = k + 1,
                                            theorem finRotate_last' {n : } :
                                            (finRotate (n + 1)) n, = 0,
                                            theorem finRotate_last {n : } :
                                            (finRotate (n + 1)) (Fin.last n) = 0
                                            theorem Fin.snoc_eq_cons_rotate {n : } {α : Type u_1} (v : Fin nα) (a : α) :
                                            Fin.snoc v a = fun (i : Fin (n + 1)) => Fin.cons a v ((finRotate (n + 1)) i)
                                            @[simp]
                                            theorem finRotate_succ_apply {n : } (i : Fin (n + 1)) :
                                            (finRotate (n + 1)) i = i + 1
                                            theorem finRotate_apply_zero {n : } :
                                            (finRotate n.succ) 0 = 1
                                            theorem coe_finRotate_of_ne_last {n : } {i : Fin n.succ} (h : i Fin.last n) :
                                            ((finRotate (n + 1)) i) = i + 1
                                            theorem coe_finRotate {n : } (i : Fin n.succ) :
                                            ((finRotate n.succ) i) = if i = Fin.last n then 0 else i + 1
                                            @[simp]
                                            theorem finProdFinEquiv_symm_apply {m : } {n : } (x : Fin (m * n)) :
                                            finProdFinEquiv.symm x = (x.divNat, x.modNat)
                                            @[simp]
                                            theorem finProdFinEquiv_apply_val {m : } {n : } (x : Fin m × Fin n) :
                                            (finProdFinEquiv x) = x.2 + n * x.1
                                            def finProdFinEquiv {m : } {n : } :
                                            Fin m × Fin n Fin (m * n)

                                            Equivalence between Fin m × Fin n and Fin (m * n)

                                            Equations
                                            • finProdFinEquiv = { toFun := fun (x : Fin m × Fin n) => x.2 + n * x.1, , invFun := fun (x : Fin (m * n)) => (x.divNat, x.modNat), left_inv := , right_inv := }
                                            Instances For
                                              @[simp]
                                              theorem Nat.divModEquiv_symm_apply (n : ) [NeZero n] (p : × Fin n) :
                                              n.divModEquiv.symm p = p.1 * n + p.2
                                              @[simp]
                                              theorem Nat.divModEquiv_apply (n : ) [NeZero n] (a : ) :
                                              n.divModEquiv a = (a / n, a)

                                              The equivalence induced by a ↦ (a / n, a % n) for nonzero n. This is like finProdFinEquiv.symm but with m infinite. See Nat.div_mod_unique for a similar propositional statement.

                                              Equations
                                              • n.divModEquiv = { toFun := fun (a : ) => (a / n, a), invFun := fun (p : × Fin n) => p.1 * n + p.2, left_inv := , right_inv := }
                                              Instances For
                                                @[simp]
                                                theorem Int.divModEquiv_symm_apply (n : ) [NeZero n] (p : × Fin n) :
                                                (Int.divModEquiv n).symm p = p.1 * n + p.2
                                                @[simp]
                                                theorem Int.divModEquiv_apply (n : ) [NeZero n] (a : ) :
                                                (Int.divModEquiv n) a = (a / n, (a.natMod n))

                                                The equivalence induced by a ↦ (a / n, a % n) for nonzero n. See Int.ediv_emod_unique for a similar propositional statement.

                                                Equations
                                                • Int.divModEquiv n = { toFun := fun (a : ) => (a / n, (a.natMod n)), invFun := fun (p : × Fin n) => p.1 * n + p.2, left_inv := , right_inv := }
                                                Instances For
                                                  @[simp]
                                                  theorem Fin.castLEquiv_apply {n : } {m : } (h : n m) (i : Fin n) :
                                                  (Fin.castLEquiv h) i = Fin.castLE h i,
                                                  @[simp]
                                                  theorem Fin.castLEquiv_symm_apply {n : } {m : } (h : n m) (i : { i : Fin m // i < n }) :
                                                  (Fin.castLEquiv h).symm i = i,
                                                  def Fin.castLEquiv {n : } {m : } (h : n m) :
                                                  Fin n { i : Fin m // i < n }

                                                  Promote a Fin n into a larger Fin m, as a subtype where the underlying values are retained.

                                                  This is the Equiv version of Fin.castLE.

                                                  Equations
                                                  • Fin.castLEquiv h = { toFun := fun (i : Fin n) => Fin.castLE h i, , invFun := fun (i : { i : Fin m // i < n }) => i, , left_inv := , right_inv := }
                                                  Instances For

                                                    Fin 0 is a subsingleton.

                                                    Equations

                                                    Fin 1 is a subsingleton.

                                                    Equations