Documentation

Mathlib.Data.Vector3

Alternate definition of Vector in terms of Fin2 #

This file provides a locale Vector3 which overrides the [a, b, c] notation to create a Vector3 instead of a List.

The :: notation is also overloaded by this file to mean Vector3.cons.

def Vector3 (α : Type u) (n : ) :

Alternate definition of Vector based on Fin2.

Instances For
    instance instInhabitedVector3 {α : Type u_1} {n : } [Inhabited α] :
    @[match_pattern]
    def Vector3.nil {α : Type u_1} :
    Vector3 α 0

    The empty vector

    Instances For
      @[match_pattern]
      def Vector3.cons {α : Type u_1} {n : } (a : α) (v : Vector3 α n) :

      The vector cons operation

      Instances For
        @[simp]
        theorem Vector3.cons_fz {α : Type u_1} {n : } (a : α) (v : Vector3 α n) :
        Vector3.cons a v Fin2.fz = a
        @[simp]
        theorem Vector3.cons_fs {α : Type u_1} {n : } (a : α) (v : Vector3 α n) (i : Fin2 n) :
        Vector3.cons a v (Fin2.fs i) = v i
        @[reducible]
        def Vector3.nth {α : Type u_1} {n : } (i : Fin2 n) (v : Vector3 α n) :
        α

        Get the ith element of a vector

        Instances For
          @[reducible]
          def Vector3.ofFn {α : Type u_1} {n : } (f : Fin2 nα) :
          Vector3 α n

          Construct a vector from a function on Fin2.

          Instances For
            def Vector3.head {α : Type u_1} {n : } (v : Vector3 α (Nat.succ n)) :
            α

            Get the head of a nonempty vector.

            Instances For
              def Vector3.tail {α : Type u_1} {n : } (v : Vector3 α (Nat.succ n)) :
              Vector3 α n

              Get the tail of a nonempty vector.

              Instances For
                theorem Vector3.eq_nil {α : Type u_1} (v : Vector3 α 0) :
                v = []
                def Vector3.nilElim {α : Type u_1} {C : Vector3 α 0Sort u} (H : C []) (v : Vector3 α 0) :
                C v

                Eliminator for an empty vector.

                Instances For
                  def Vector3.consElim {α : Type u_1} {n : } {C : Vector3 α (Nat.succ n)Sort u} (H : (a : α) → (t : Vector3 α n) → C (Vector3.cons a t)) (v : Vector3 α (Nat.succ n)) :
                  C v

                  Recursion principle for a nonempty vector.

                  Instances For
                    @[simp]
                    theorem Vector3.consElim_cons {α : Type u_1} {n : } {C : Vector3 α (Nat.succ n)Sort u_2} {H : (a : α) → (t : Vector3 α n) → C (Vector3.cons a t)} {a : α} {t : Vector3 α n} :
                    def Vector3.recOn {α : Type u_1} {C : {n : } → Vector3 α nSort u} {n : } (v : Vector3 α n) (H0 : C 0 []) (Hs : {n : } → (a : α) → (w : Vector3 α n) → C n wC (Nat.succ n) (Vector3.cons a w)) :
                    C n v

                    Recursion principle with the vector as first argument.

                    Equations
                    Instances For
                      @[simp]
                      theorem Vector3.recOn_nil {α : Type u_1} {C : {n : } → Vector3 α nSort u_2} {H0 : C 0 []} {Hs : {n : } → (a : α) → (w : Vector3 α n) → C n wC (Nat.succ n) (Vector3.cons a w)} :
                      Vector3.recOn [] H0 Hs = H0
                      @[simp]
                      theorem Vector3.recOn_cons {α : Type u_1} {C : {n : } → Vector3 α nSort u_2} {H0 : C 0 []} {Hs : {n : } → (a : α) → (w : Vector3 α n) → C n wC (Nat.succ n) (Vector3.cons a w)} {n : } {a : α} {v : Vector3 α n} :
                      Vector3.recOn (Vector3.cons a v) H0 Hs = Hs n a v (Vector3.recOn v H0 Hs)
                      def Vector3.append {α : Type u_1} {m : } {n : } (v : Vector3 α m) (w : Vector3 α n) :
                      Vector3 α (n + m)

                      Append two vectors

                      Instances For
                        @[simp]
                        theorem Vector3.append_nil {α : Type u_1} {n : } (w : Vector3 α n) :
                        @[simp]
                        theorem Vector3.append_cons {α : Type u_1} {m : } {n : } (a : α) (v : Vector3 α m) (w : Vector3 α n) :
                        @[simp]
                        theorem Vector3.append_left {α : Type u_1} {m : } (i : Fin2 m) (v : Vector3 α m) {n : } (w : Vector3 α n) :
                        Vector3.append v w (Fin2.left n i) = v i
                        @[simp]
                        theorem Vector3.append_add {α : Type u_1} {m : } (v : Vector3 α m) {n : } (w : Vector3 α n) (i : Fin2 n) :
                        Vector3.append v w (Fin2.add i m) = w i
                        def Vector3.insert {α : Type u_1} {n : } (a : α) (v : Vector3 α n) (i : Fin2 (Nat.succ n)) :

                        Insert a into v at index i.

                        Instances For
                          @[simp]
                          theorem Vector3.insert_fz {α : Type u_1} {n : } (a : α) (v : Vector3 α n) :
                          Vector3.insert a v Fin2.fz = Vector3.cons a v
                          @[simp]
                          theorem Vector3.insert_fs {α : Type u_1} {n : } (a : α) (b : α) (v : Vector3 α n) (i : Fin2 (Nat.succ n)) :
                          theorem Vector3.append_insert {α : Type u_1} {m : } {n : } (a : α) (t : Vector3 α m) (v : Vector3 α n) (i : Fin2 (Nat.succ n)) (e : Nat.succ n + m = Nat.succ (n + m)) :
                          def VectorEx {α : Type u_1} (k : ) :
                          (Vector3 α kProp) → Prop

                          "Curried" exists, i.e. ∃ x₁ ... xₙ, f [x₁, ..., xₙ].

                          Equations
                          Instances For
                            def VectorAll {α : Type u_1} (k : ) :
                            (Vector3 α kProp) → Prop

                            "Curried" forall, i.e. ∀ x₁ ... xₙ, f [x₁, ..., xₙ].

                            Equations
                            Instances For
                              theorem exists_vector_zero {α : Type u_1} (f : Vector3 α 0Prop) :
                              Exists f f []
                              theorem exists_vector_succ {α : Type u_1} {n : } (f : Vector3 α (Nat.succ n)Prop) :
                              Exists f x v, f (Vector3.cons x v)
                              theorem vectorEx_iff_exists {α : Type u_1} {n : } (f : Vector3 α nProp) :
                              theorem vectorAll_iff_forall {α : Type u_1} {n : } (f : Vector3 α nProp) :
                              VectorAll n f (v : Vector3 α n) → f v
                              def VectorAllP {α : Type u_1} {n : } (p : αProp) (v : Vector3 α n) :

                              VectorAllP p v is equivalent to ∀ i, p (v i), but unfolds directly to a conjunction, i.e. VectorAllP p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

                              Instances For
                                @[simp]
                                theorem vectorAllP_nil {α : Type u_1} (p : αProp) :
                                @[simp]
                                theorem vectorAllP_singleton {α : Type u_1} (p : αProp) (x : α) :
                                VectorAllP p [x] = p x
                                @[simp]
                                theorem vectorAllP_cons {α : Type u_1} {n : } (p : αProp) (x : α) (v : Vector3 α n) :
                                theorem vectorAllP_iff_forall {α : Type u_1} {n : } (p : αProp) (v : Vector3 α n) :
                                VectorAllP p v (i : Fin2 n) → p (v i)
                                theorem VectorAllP.imp {α : Type u_1} {n : } {p : αProp} {q : αProp} (h : (x : α) → p xq x) {v : Vector3 α n} (al : VectorAllP p v) :