Documentation

Mathlib.Logic.Equiv.Fin.Basic

Equivalences for Fin n #

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

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

      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 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.castSucc and i.succ to i.

          Equations
            Instances For
              @[simp]
              theorem finSuccEquiv'_at {n : } (i : Fin (n + 1)) :
              @[simp]
              theorem finSuccEquiv'_succAbove {n : } (i : Fin (n + 1)) (j : Fin n) :
              theorem finSuccEquiv'_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
              theorem finSuccEquiv'_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
              @[simp]
              theorem finSuccEquiv'_symm_none {n : } (i : Fin (n + 1)) :
              @[simp]
              theorem finSuccEquiv'_symm_some {n : } (i : Fin (n + 1)) (j : Fin n) :
              @[simp]
              theorem finSuccEquiv'_eq_some {n : } {i j : Fin (n + 1)} {k : Fin n} :
              @[simp]
              theorem finSuccEquiv'_eq_none {n : } {i j : Fin (n + 1)} :
              theorem finSuccEquiv'_symm_some_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
              theorem finSuccEquiv'_symm_some_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
              theorem finSuccEquiv'_symm_coe_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
              theorem finSuccEquiv'_symm_coe_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
              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 : } :
                  @[simp]
                  theorem finSuccEquiv_succ {n : } (m : Fin n) :
                  @[simp]
                  theorem finSuccEquiv_symm_some {n : } (m : Fin n) :
                  @[simp]
                  theorem finSuccEquiv_eq_some {n : } {i : Fin (n + 1)} {j : Fin n} :
                  (finSuccEquiv n) i = some j i = j.succ
                  @[simp]
                  theorem finSuccEquiv_eq_none {n : } {i : Fin (n + 1)} :
                  (finSuccEquiv n) i = none i = 0
                  theorem finSuccEquiv'_last_apply {n : } {i : Fin (n + 1)} (h : i Fin.last n) :
                  theorem finSuccEquiv'_ne_last_apply {n : } {i 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) :
                      theorem finSuccAboveEquiv_symm_apply_last {n : } (x : { x : Fin (n + 1) // x Fin.last n }) :
                      theorem finSuccAboveEquiv_symm_apply_ne_last {n : } {p : Fin (n + 1)} (h : p Fin.last n) (x : { x : Fin (n + 1) // x p }) :
                      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
                          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) ι) :
                              ((embeddingFinSucc n ι) e).fst = e Fin.succ
                              @[simp]
                              theorem Equiv.embeddingFinSucc_snd {n : } {ι : Type u_1} (e : Fin (n + 1) ι) :
                              ((embeddingFinSucc n ι) e).snd = e 0
                              @[simp]
                              theorem Equiv.coe_embeddingFinSucc_symm {n : } {ι : Type u_1} (f : (e : Fin n ι) × { i : ι // iSet.range e }) :
                              ((embeddingFinSucc n ι).symm f) = Fin.cons f.snd f.fst
                              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]
                                  @[simp]
                                  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 : ) :
                                      @[simp]
                                      theorem finAddFlip_apply_natAdd {n : } (k : Fin n) (m : ) :
                                      @[simp]
                                      theorem finAddFlip_apply_mk_left {m n k : } (h : k < m) (hk : k < m + n := ) (hnk : 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 finProdFinEquiv {m n : } :
                                      Fin m × Fin n Fin (m * n)

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

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem finProdFinEquiv_apply_val {m n : } (x : Fin m × Fin n) :
                                          (finProdFinEquiv x) = x.2 + n * x.1
                                          @[simp]

                                          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
                                            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. See Int.ediv_emod_unique for a similar propositional statement.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Int.divModEquiv_symm_apply (n : ) [NeZero n] (p : × Fin n) :
                                                  (divModEquiv n).symm p = p.1 * n + p.2
                                                  @[simp]
                                                  theorem Int.divModEquiv_apply (n : ) [NeZero n] (a : ) :
                                                  (divModEquiv n) a = (a / n, (a.natMod n))
                                                  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
                                                    Instances For
                                                      @[simp]
                                                      theorem Fin.castLEquiv_apply {n m : } (h : n m) (i : Fin n) :
                                                      (castLEquiv h) i = castLE h i,
                                                      @[simp]
                                                      theorem Fin.castLEquiv_symm_apply {n m : } (h : n m) (i : { i : Fin m // i < n }) :
                                                      (castLEquiv h).symm i = i,

                                                      Fin 0 is a subsingleton.

                                                      Fin 1 is a subsingleton.

                                                      def Fin.appendEquiv {α : Type u_1} (m n : ) :
                                                      (Fin mα) × (Fin nα) (Fin (m + n)α)

                                                      The natural Equiv between (Fin m → α) × (Fin n → α) and Fin (m + n) → α

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Fin.appendEquiv_apply {α : Type u_1} (m n : ) (fg : (Fin mα) × (Fin nα)) (a✝ : Fin (m + n)) :
                                                          (appendEquiv m n) fg a✝ = append fg.1 fg.2 a✝
                                                          @[simp]
                                                          theorem Fin.appendEquiv_symm_apply {α : Type u_1} (m n : ) (f : Fin (m + n)α) :
                                                          (appendEquiv m n).symm f = (fun (i : Fin m) => f (castAdd n i), fun (i : Fin n) => f (natAdd m i))