data.vector3 - mathlib3 docs

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

source

@[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

v.rec_on H0 Hs = n.rec_on (λ (v : vector3 α 0), vector3.nil_elim H0 v) (λ (n : ℕ) (IH : Π (_a : vector3 α n), C _a) (v : vector3 α n.succ), vector3.cons_elim (λ (a : α) (t : vector3 α n), Hs a t (IH t)) v) v

source

@[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)} :

vector3.nil.rec_on H0 Hs = H0

source

@[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)

source

def vector3.append {α : Type u_1} {m n : ℕ} (v : vector3 α m) (w : vector3 α n) :

vector3 α (n + m)

Append two vectors

Equations

v.append w = m.rec_on (λ (_x : vector3 α 0), w) (λ (m : ℕ) (IH : vector3 α m → vector3 α (n + m)) (v : vector3 α m.succ), vector3.cons_elim (λ (a : α) (t : vector3 α m), fin2.cases' a (IH t)) v) v

source

@[simp]

theorem vector3.append_nil {α : Type u_1} {n : ℕ} (w : vector3 α n) :

vector3.nil.append w = w

source

@[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

source

@[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

source

@[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

source

def vector3.insert {α : Type u_1} {n : ℕ} (a : α) (v : vector3 α n) (i : fin2 n.succ) :

vector3 α n.succ

Insert a into v at index i.

Equations

vector3.insert a v i = λ (j : fin2 n.succ), (a::v) (i.insert_perm j)

source

@[simp]

theorem vector3.insert_fz {α : Type u_1} {n : ℕ} (a : α) (v : vector3 α n) :

vector3.insert a v fin2.fz = a::v

source

@[simp]

theorem vector3.insert_fs {α : Type u_1} {n : ℕ} (a b : α) (v : vector3 α n) (i : fin2 n.succ) :

vector3.insert a (b::v) i.fs = b::vector3.insert a v i

source

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))

source

def vector_ex {α : Type u_1} (k : ℕ) :

(vector3 α k → Prop) → Prop

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

Equations

vector_ex k.succ f = ∃ (x : α), vector_ex k (λ (v : vector3 α k), f (x::v))
vector_ex 0 f = f vector3.nil

source

def vector_all {α : Type u_1} (k : ℕ) :

(vector3 α k → Prop) → Prop

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

Equations

vector_all k.succ f = ∀ (x : α), vector_all k (λ (v : vector3 α k), f (x::v))
vector_all 0 f = f vector3.nil

source

theorem exists_vector_zero {α : Type u_1} (f : vector3 α 0 → Prop) :

Exists f ↔ f vector3.nil

source

theorem exists_vector_succ {α : Type u_1} {n : ℕ} (f : vector3 α n.succ → Prop) :

Exists f ↔ ∃ (x : α) (v : vector3 α n), f (x::v)

source

theorem vector_ex_iff_exists {α : Type u_1} {n : ℕ} (f : vector3 α n → Prop) :

vector_ex n f ↔ Exists f

source

theorem vector_all_iff_forall {α : Type u_1} {n : ℕ} (f : vector3 α n → Prop) :

vector_all n f ↔ ∀ (v : vector3 α n), f v

source

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

vector_allp p v = v.rec_on true (λ (n : ℕ) (a : α) (v : vector3 α n) (IH : Prop), v.rec_on (p a) (λ (n : ℕ) (b : α) (v' : vector3 α n) (_x : (λ (n : ℕ) (v : vector3 α n), Prop) n v'), p a ∧ IH))