# 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.

Equations
Instances For
instance instInhabitedVector3 {α : Type u_1} {n : } [] :
Equations
• instInhabitedVector3 = { default := fun (x : Fin2 n) => default }
@[match_pattern]
def Vector3.nil {α : Type u_1} :
Vector3 α 0

The empty vector

Equations
• [] = nomatch a
Instances For
@[match_pattern]
def Vector3.cons {α : Type u_1} {n : } (a : α) (v : Vector3 α n) :
Vector3 α (n + 1)

The vector cons operation

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For

The vector cons operation

Equations
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 i.fs = v i
@[reducible, inline]
abbrev Vector3.nth {α : Type u_1} {n : } (i : Fin2 n) (v : Vector3 α n) :
α

Get the ith element of a vector

Equations
• = v i
Instances For
@[reducible, inline]
abbrev Vector3.ofFn {α : Type u_1} {n : } (f : Fin2 nα) :
Vector3 α n

Construct a vector from a function on Fin2.

Equations
Instances For
def Vector3.head {α : Type u_1} {n : } (v : Vector3 α (n + 1)) :
α

Get the head of a nonempty vector.

Equations
Instances For
def Vector3.tail {α : Type u_1} {n : } (v : Vector3 α (n + 1)) :
Vector3 α n

Get the tail of a nonempty vector.

Equations
• v.tail i = v i.fs
Instances For
theorem Vector3.eq_nil {α : Type u_1} (v : Vector3 α 0) :
v = []
theorem Vector3.cons_head_tail {α : Type u_1} {n : } (v : Vector3 α (n + 1)) :
def Vector3.nilElim {α : Type u_1} {C : Vector3 α 0Sort u} (H : C []) (v : Vector3 α 0) :
C v

Eliminator for an empty vector.

Equations
• = .mpr H
Instances For
def Vector3.consElim {α : Type u_1} {n : } {C : Vector3 α (n + 1)Sort u} (H : (a : α) → (t : Vector3 α n) → C (Vector3.cons a t)) (v : Vector3 α (n + 1)) :
C v

Recursion principle for a nonempty vector.

Equations
• = .mpr (H v.head v.tail)
Instances For
@[simp]
theorem Vector3.consElim_cons {α : Type u_1} {n : } {C : Vector3 α (n + 1)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 []) (Hs : {n : } → (a : α) → (w : Vector3 α n) → C wC (Vector3.cons a w)) :
C 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 []} {Hs : {n : } → (a : α) → (w : Vector3 α n) → C wC (Vector3.cons a w)} :
[].recOn H0 Hs = H0
@[simp]
theorem Vector3.recOn_cons {α : Type u_1} {C : {n : } → Vector3 α nSort u_2} {H0 : C []} {Hs : {n : } → (a : α) → (w : Vector3 α n) → C wC (Vector3.cons a w)} {n : } {a : α} {v : Vector3 α n} :
(Vector3.cons a v).recOn H0 Hs = Hs a v (v.recOn H0 Hs)
def Vector3.append {α : Type u_1} {m : } {n : } (v : Vector3 α m) (w : Vector3 α n) :
Vector3 α (n + m)

Append two vectors

Equations
Instances For
@[simp]
theorem Vector3.append_nil {α : Type u_1} {n : } (w : Vector3 α n) :
[].append w = w
@[simp]
theorem Vector3.append_cons {α : Type u_1} {m : } {n : } (a : α) (v : Vector3 α m) (w : Vector3 α n) :
(Vector3.cons a v).append w = Vector3.cons a (v.append w)
@[simp]
theorem Vector3.append_left {α : Type u_1} {m : } (i : Fin2 m) (v : Vector3 α m) {n : } (w : Vector3 α n) :
v.append 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) :
v.append w (i.add m) = w i
def Vector3.insert {α : Type u_1} {n : } (a : α) (v : Vector3 α n) (i : Fin2 (n + 1)) :
Vector3 α (n + 1)

Insert a into v at index i.

Equations
Instances For
@[simp]
theorem Vector3.insert_fz {α : Type u_1} {n : } (a : α) (v : Vector3 α n) :
Vector3.insert a v Fin2.fz =
@[simp]
theorem Vector3.insert_fs {α : Type u_1} {n : } (a : α) (b : α) (v : Vector3 α n) (i : Fin2 (n + 1)) :
theorem Vector3.append_insert {α : Type u_1} {m : } {n : } (a : α) (t : Vector3 α m) (v : Vector3 α n) (i : Fin2 (n + 1)) (e : n + 1 + m = n + m + 1) :
Vector3.insert a (t.append v) (Eq.recOn e (i.add m)) = Eq.recOn e (t.append (Vector3.insert a v i))
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) :
f []
theorem exists_vector_succ {α : Type u_1} {n : } (f : Vector3 α n.succProp) :
∃ (x : α) (v : Vector3 α n), 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) :
∀ (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.

Equations
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) :
∀ (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 : ) :