mathlib documentation

data.array.lemmas

@[protected, instance]
def d_array.inhabited {n : } {α : fin nType u} [Π (i : fin n), inhabited (α i)] :
Equations
@[protected, instance]
def array.inhabited {n : } {α : Type u_1} [inhabited α] :
Equations
theorem array.to_list_of_heq {n₁ n₂ : } {α : Type u_1} {a₁ : array n₁ α} {a₂ : array n₂ α} (hn : n₁ = n₂) (ha : a₁ == a₂) :
a₁.to_list = a₂.to_list
theorem array.rev_list_reverse_aux {n : } {α : Type u} {a : array n α} (i : ) (h : i n) (t : list α) :
(d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil).reverse_core t = d_array.rev_iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h t
@[simp]
theorem array.rev_list_reverse {n : } {α : Type u} {a : array n α} :
@[simp]
theorem array.to_list_reverse {n : } {α : Type u} {a : array n α} :
theorem array.mem.def {n : } {α : Type u} {v : α} {a : array n α} :
v a ∃ (i : fin n), a.read i = v
theorem array.mem_rev_list_aux {n : } {α : Type u} {v : α} {a : array n α} {i : } (h : i n) :
(∃ (j : fin n), j < i a.read j = v) v d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil
@[simp]
theorem array.mem_rev_list {n : } {α : Type u} {v : α} {a : array n α} :
@[simp]
theorem array.mem_to_list {n : } {α : Type u} {v : α} {a : array n α} :
v a.to_list v a
theorem array.rev_list_foldr_aux {n : } {α : Type u} {β : Type w} {b : β} {f : α → β → β} {a : array n α} {i : } (h : i n) :
list.foldr f b (d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil) = d_array.iterate_aux a (λ (_x : fin n), f) i h b
theorem array.rev_list_foldr {n : } {α : Type u} {β : Type w} {b : β} {f : α → β → β} {a : array n α} :
theorem array.to_list_foldl {n : } {α : Type u} {β : Type w} {b : β} {f : β → α → β} {a : array n α} :
theorem array.rev_list_length_aux {n : } {α : Type u} (a : array n α) (i : ) (h : i n) :
(d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil).length = i
@[simp]
theorem array.rev_list_length {n : } {α : Type u} (a : array n α) :
@[simp]
theorem array.to_list_length {n : } {α : Type u} (a : array n α) :
theorem array.to_list_nth_le_aux {n : } {α : Type u} {a : array n α} (i : ) (ih : i < n) (j : ) {jh : j n} {t : list α} {h' : i < (d_array.rev_iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) j jh t).length} :
(∀ (k : ) (tl : k < t.length), j + k = it.nth_le k tl = a.read i, ih⟩)(d_array.rev_iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) j jh t).nth_le i h' = a.read i, ih⟩
theorem array.to_list_nth_le {n : } {α : Type u} {a : array n α} (i : ) (h : i < n) (h' : i < a.to_list.length) :
a.to_list.nth_le i h' = a.read i, h⟩
@[simp]
theorem array.to_list_nth_le' {n : } {α : Type u} (a : array n α) (i : fin n) (h' : i < a.to_list.length) :
a.to_list.nth_le i h' = a.read i
theorem array.to_list_nth {n : } {α : Type u} {a : array n α} {i : } {v : α} :
a.to_list.nth i = some v ∃ (h : i < n), a.read i, h⟩ = v
theorem array.write_to_list {n : } {α : Type u} {a : array n α} {i : fin n} {v : α} :
theorem array.mem_to_list_enum {n : } {α : Type u} {a : array n α} {i : } {v : α} :
(i, v) a.to_list.enum ∃ (h : i < n), a.read i, h⟩ = v
@[simp]
theorem array.to_list_to_array {n : } {α : Type u} (a : array n α) :
@[simp]
theorem array.to_array_to_list {α : Type u} (l : list α) :
theorem array.push_back_rev_list_aux {n : } {α : Type u} {v : α} {a : array n α} (i : ) (h : i n + 1) (h' : i n) :
d_array.iterate_aux (a.push_back v) (λ (_x : fin (n + 1)), λ (_x : α) (_y : list α), _x :: _y) i h list.nil = d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h' list.nil
@[simp]
theorem array.push_back_rev_list {n : } {α : Type u} {v : α} {a : array n α} :
@[simp]
theorem array.push_back_to_list {n : } {α : Type u} {v : α} {a : array n α} :
@[simp]
theorem array.read_push_back_left {n : } {α : Type u} {v : α} {a : array n α} (i : fin n) :
@[simp]
theorem array.read_push_back_right {n : } {α : Type u} {v : α} {a : array n α} :
(a.push_back v).read (fin.last n) = v
@[simp]
theorem array.read_foreach {n : } {α : Type u} {β : Type v} {i : fin n} {f : fin nα → β} {a : array n α} :
(a.foreach f).read i = f i (a.read i)
theorem array.read_map {n : } {α : Type u} {β : Type v} {i : fin n} {f : α → β} {a : array n α} :
(a.map f).read i = f (a.read i)
@[simp]
theorem array.read_map₂ {n : } {α : Type u} {i : fin n} {f : α → α → α} {a₁ a₂ : array n α} :
(array.map₂ f a₁ a₂).read i = f (a₁.read i) (a₂.read i)
def equiv.d_array_equiv_fin {n : } (α : fin nType u_1) :
d_array n α Π (i : fin n), α i

The natural equivalence between length-n heterogeneous arrays and dependent functions from fin n.

Equations
def equiv.array_equiv_fin (n : ) (α : Type u_1) :
array n α (fin n → α)

The natural equivalence between length-n arrays and functions from fin n.

Equations
def equiv.vector_equiv_array (α : Type u_1) (n : ) :
vector α n array n α

The natural equivalence between length-n vectors and length-n arrays.

Equations
@[protected, instance]
Equations