data.vector3

# Alternate definition of vector in terms of fin2#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 vector3
@[protected, instance]
def vector3.inhabited {α : Type u_1} {n : } [inhabited α] :
Equations
def vector3.nil {α : Type u_1} :
0

The empty vector

def vector3.cons {α : Type u_1} {n : } (a : α) (v : n) :
n.succ

The vector cons operation

Equations
@[simp]
theorem vector3.cons_fz {α : Type u_1} {n : } (a : α) (v : n) :
(a::v) fin2.fz = a
@[simp]
theorem vector3.cons_fs {α : Type u_1} {n : } (a : α) (v : n) (i : fin2 n) :
(a::v) i.fs = v i
@[reducible]
def vector3.nth {α : Type u_1} {n : } (i : fin2 n) (v : n) :
α

Get the ith element of a vector

Equations
• v = v i
@[reducible]
def vector3.of_fn {α : Type u_1} {n : } (f : fin2 n α) :
n

Construct a vector from a function on fin2.

Equations
def vector3.head {α : Type u_1} {n : } (v : n.succ) :
α

Get the head of a nonempty vector.

Equations
def vector3.tail {α : Type u_1} {n : } (v : n.succ) :
n

Get the tail of a nonempty vector.

Equations
theorem vector3.eq_nil {α : Type u_1} (v : 0) :
theorem vector3.cons_head_tail {α : Type u_1} {n : } (v : n.succ) :
def vector3.nil_elim {α : Type u_1} {C : 0 Sort u} (H : C vector3.nil) (v : 0) :
C v

Eliminator for an empty vector.

Equations
def vector3.cons_elim {α : Type u_1} {n : } {C : n.succ Sort u} (H : Π (a : α) (t : n), C (a::t)) (v : n.succ) :
C v

Recursion principle for a nonempty vector.

Equations
@[simp]
theorem vector3.cons_elim_cons {α : Type u_1} {n : } {C : n.succ Sort u_2} {H : Π (a : α) (t : n), C (a::t)} {a : α} {t : n} :
(a::t) = H a t
@[protected]
def vector3.rec_on {α : Type u_1} {C : Π {n : }, n Sort u} {n : } (v : n) (H0 : C vector3.nil) (Hs : Π {n : } (a : α) (w : n), C w C (a::w)) :
C v

Recursion principle with the vector as first argument.

Equations
@[simp]
theorem vector3.rec_on_nil {α : Type u_1} {C : Π {n : }, n Sort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : n), C w C (a::w)} :
Hs = H0
@[simp]
theorem vector3.rec_on_cons {α : Type u_1} {C : Π {n : }, n Sort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : n), C w C (a::w)} {n : } {a : α} {v : n} :
(a::v).rec_on H0 Hs = Hs a v (v.rec_on H0 Hs)
def vector3.append {α : Type u_1} {m n : } (v : m) (w : n) :
(n + m)

Append two vectors

Equations
@[simp]
theorem vector3.append_nil {α : Type u_1} {n : } (w : n) :
@[simp]
theorem vector3.append_cons {α : Type u_1} {m n : } (a : α) (v : m) (w : n) :
(a::v).append w = a::v.append w
@[simp]
theorem vector3.append_left {α : Type u_1} {m : } (i : fin2 m) (v : m) {n : } (w : n) :
v.append w i) = v i
@[simp]
theorem vector3.append_add {α : Type u_1} {m : } (v : m) {n : } (w : n) (i : fin2 n) :
v.append w (i.add m) = w i
def vector3.insert {α : Type u_1} {n : } (a : α) (v : n) (i : fin2 n.succ) :
n.succ

Insert a into v at index i.

Equations
@[simp]
theorem vector3.insert_fz {α : Type u_1} {n : } (a : α) (v : n) :
= a::v
@[simp]
theorem vector3.insert_fs {α : Type u_1} {n : } (a b : α) (v : n) (i : fin2 n.succ) :
(b::v) i.fs = b:: i
theorem vector3.append_insert {α : Type u_1} {m n : } (a : α) (t : m) (v : n) (i : fin2 n.succ) (e : n.succ + m = (n + m).succ) :
(t.append v) (e.rec_on (i.add m)) = e.rec_on (t.append v i))
def vector_ex {α : Type u_1} (k : ) :
(vector3 α k Prop) Prop

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

Equations
• f = (x : α), (λ (v : k), f (x::v))
• f =
def vector_all {α : Type u_1} (k : ) :
(vector3 α k Prop) Prop

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

Equations
• f = (x : α), (λ (v : k), f (x::v))
• f =
theorem exists_vector_zero {α : Type u_1} (f : 0 Prop) :
theorem exists_vector_succ {α : Type u_1} {n : } (f : n.succ Prop) :
(x : α) (v : n), f (x::v)
theorem vector_ex_iff_exists {α : Type u_1} {n : } (f : n Prop) :
f
theorem vector_all_iff_forall {α : Type u_1} {n : } (f : n Prop) :
f (v : n), f v
def vector_allp {α : Type u_1} {n : } (p : α Prop) (v : n) :
Prop

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

Equations
• v = (λ (n : ) (a : α) (v : n) (IH : Prop), v.rec_on (p a) (λ (n : ) (b : α) (v' : n) (_x : (λ (n : ) (v : n), Prop) n v'), p a IH))
@[simp]
theorem vector_allp_nil {α : Type u_1} (p : α Prop) :
@[simp]
theorem vector_allp_singleton {α : Type u_1} (p : α Prop) (x : α) :
= p x
@[simp]
theorem vector_allp_cons {α : Type u_1} {n : } (p : α Prop) (x : α) (v : n) :
(x::v) p x v
theorem vector_allp_iff_forall {α : Type u_1} {n : } (p : α Prop) (v : n) :
v (i : fin2 n), p (v i)
theorem vector_allp.imp {α : Type u_1} {n : } {p q : α Prop} (h : (x : α), p x q x) {v : n} (al : v) :
v