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
.
@[protected, instance]
Equations
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
- vector3.nil_elim H v = _.mpr H
@[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
@[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
Append two vectors
@[simp]
Insert a
into v
at index i
.
Equations
- vector3.insert a v i = λ (j : fin2 n.succ), (a::v) (i.insert_perm j)
@[simp]
theorem
vector3.insert_fz
{α : Type u_1}
{n : ℕ}
(a : α)
(v : vector3 α n) :
vector3.insert a v fin2.fz = a::v
@[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
"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
theorem
vector_all_iff_forall
{α : Type u_1}
{n : ℕ}
(f : vector3 α n → Prop) :
vector_all n f ↔ ∀ (v : vector3 α n), f v
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
.
@[simp]
@[simp]
theorem
vector_allp_singleton
{α : Type u_1}
(p : α → Prop)
(x : α) :
vector_allp p (x::vector3.nil) = p x
@[simp]
theorem
vector_allp_cons
{α : Type u_1}
{n : ℕ}
(p : α → Prop)
(x : α)
(v : vector3 α n) :
vector_allp p (x::v) ↔ p x ∧ vector_allp p v
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) :
vector_allp q v