mathlib documentation

data.vector3

Alternate definition of vector in terms of fin2 #

This file provides a locale vector3 which overrides [a, b, c] notation to create vector3 not list.

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

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

Alternate definition of vector based on fin2.

Equations
def vector3.nil {α : Type u_1} :
vector3 α 0

The empty vector

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

The vector cons operation

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

Get the ith element of a vector

Equations
def vector3.of_fn {α : Type u_1} {n : } (f : fin2 n → α) :
vector3 α n

Construct a vector from a function on fin2.

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

Get the head of a nonempty vector.

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

Get the tail of a nonempty vector.

Equations
theorem vector3.eq_nil {α : Type u_1} (v : vector3 α 0) :
theorem vector3.cons_head_tail {α : Type u_1} {n : } (v : vector3 α n.succ) :
def vector3.nil_elim {α : Type u_1} {C : vector3 α 0Sort u} (H : C vector3.nil) (v : vector3 α 0) :
C v
Equations
def vector3.cons_elim {α : Type u_1} {n : } {C : vector3 α n.succSort u} (H : Π (a : α) (t : vector3 α n), C (a::t)) (v : vector3 α n.succ) :
C v
Equations
@[simp]
theorem vector3.cons_elim_cons {α : Type u_1} {n : } {C : vector3 α n.succSort u_2} {H : Π (a : α) (t : vector3 α n), C (a::t)} {a : α} {t : vector3 α n} :
vector3.cons_elim H (a::t) = H a t
def vector3.rec_on {α : Type u_1} {C : Π {n : }, vector3 α nSort u} {n : } (v : vector3 α n) (H0 : C vector3.nil) (Hs : Π {n : } (a : α) (w : vector3 α n), C wC (a::w)) :
C v
Equations
@[simp]
theorem vector3.rec_on_nil {α : Type u_1} {C : Π {n : }, vector3 α nSort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : vector3 α n), C wC (a::w)} :
@[simp]
theorem vector3.rec_on_cons {α : Type u_1} {C : Π {n : }, vector3 α nSort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : vector3 α n), C wC (a::w)} {n : } {a : α} {v : vector3 α n} :
(a::v).rec_on H0 Hs = Hs a v (v.rec_on H0 Hs)
def vector3.append {α : Type u_1} {m : } (v : vector3 α m) {n : } (w : vector3 α n) :
vector3 α (n + m)

Append two vectors

Equations
@[simp]
theorem vector3.append_nil {α : Type u_1} {n : } (w : vector3 α n) :
@[simp]
theorem vector3.append_cons {α : Type u_1} (a : α) {m : } (v : vector3 α m) {n : } (w : vector3 α n) :
(a::v).append w = 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} (a : α) {n : } (v : vector3 α n) (i : fin2 n.succ) :

Insert a into v at index i.

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

"Curried" exists, i.e. ∃ x1 ... xn, f [x1, ..., xn]

Equations
def vector_all {α : Type u_1} (k : ) :
(vector3 α k → Prop) → Prop

"Curried" forall, i.e. ∀ x1 ... xn, f [x1, ..., xn]

Equations
theorem exists_vector_zero {α : Type u_1} (f : vector3 α 0 → Prop) :
theorem exists_vector_succ {α : Type u_1} {n : } (f : vector3 α n.succ → Prop) :
Exists f ∃ (x : α) (v : vector3 α n), f (x::v)
theorem vector_ex_iff_exists {α : Type u_1} {n : } (f : vector3 α n → Prop) :
theorem vector_all_iff_forall {α : Type u_1} {n : } (f : vector3 α n → Prop) :
vector_all n f ∀ (v : vector3 α n), f v
def vector_allp {α : Type u_1} (p : α → Prop) {n : } (v : vector3 α 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
@[simp]
theorem vector_allp_nil {α : Type u_1} (p : α → Prop) :
@[simp]
theorem vector_allp_singleton {α : Type u_1} (p : α → Prop) (x : α) :
@[simp]
theorem vector_allp_cons {α : Type u_1} (p : α → Prop) {n : } (x : α) (v : vector3 α n) :
theorem vector_allp_iff_forall {α : Type u_1} (p : α → Prop) {n : } (v : vector3 α n) :
vector_allp p v ∀ (i : fin2 n), p (v i)
theorem vector_allp.imp {α : Type u_1} {p q : α → Prop} (h : ∀ (x : α), p xq x) {n : } {v : vector3 α n} (al : vector_allp p v) :