mathlib3 documentation

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} :
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
@[reducible]
def vector3.nth {α : Type u_1} {n : } (i : fin2 n) (v : vector3 α n) :
α

Get the ith element of a vector

Equations
@[reducible]
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 α 0 Sort u} (H : C vector3.nil) (v : vector3 α 0) :
C v

Eliminator for an empty vector.

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

Recursion principle for a nonempty vector.

Equations
@[simp]
theorem vector3.cons_elim_cons {α : Type u_1} {n : } {C : vector3 α n.succ Sort u_2} {H : Π (a : α) (t : vector3 α n), C (a::t)} {a : α} {t : vector3 α n} :
vector3.cons_elim H (a::t) = H a t
@[protected]
def vector3.rec_on {α : Type u_1} {C : Π {n : }, vector3 α n Sort u} {n : } (v : vector3 α n) (H0 : C vector3.nil) (Hs : Π {n : } (a : α) (w : vector3 α 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 : }, vector3 α n Sort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : vector3 α n), C w C (a::w)} :
@[simp]
theorem vector3.rec_on_cons {α : Type u_1} {C : Π {n : }, vector3 α n Sort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : vector3 α n), C w C (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 n : } (v : vector3 α m) (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} {m n : } (a : α) (v : vector3 α m) (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} {n : } (a : α) (v : vector3 α n) (i : fin2 n.succ) :

Insert a into v at index i.

Equations
@[simp]
theorem vector3.insert_fz {α : Type u_1} {n : } (a : α) (v : vector3 α n) :
@[simp]
theorem vector3.insert_fs {α : Type u_1} {n : } (a b : α) (v : vector3 α n) (i : fin2 n.succ) :
theorem vector3.append_insert {α : Type u_1} {m n : } (a : α) (t : vector3 α m) (v : vector3 α n) (i : fin2 n.succ) (e : n.succ + m = (n + m).succ) :
vector3.insert a (t.append v) (e.rec_on (i.add m)) = 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. ∃ x₁ ... xₙ, f [x₁, ..., xₙ].

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

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

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} {n : } (p : α Prop) (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} {n : } (p : α Prop) (x : α) (v : vector3 α n) :
theorem vector_allp_iff_forall {α : Type u_1} {n : } (p : α Prop) (v : vector3 α n) :
vector_allp p 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 : vector3 α n} (al : vector_allp p v) :