Documentation

Mathlib.Data.Array.ExtractLemmas

Lemmas about Array.extract #

Some useful lemmas about Array.extract

@[simp]
theorem Array.extract_eq_nil_of_start_eq_end {α : Type u} {i : Nat} {a : Array α} :
a.extract i i = #[]
theorem Array.extract_append_left {α : Type u} {a : Array α} {b : Array α} {i : Nat} {j : Nat} (h : j a.size) :
(a ++ b).extract i j = a.extract i j
theorem Array.extract_append_right {α : Type u} {a : Array α} {b : Array α} {i : Nat} {j : Nat} (h : a.size i) :
(a ++ b).extract i j = b.extract (i - a.size) (j - a.size)
theorem Array.extract_eq_of_size_le_end {α : Type u} {l : Nat} {p : Nat} {a : Array α} (h : a.size l) :
a.extract p l = a.extract p a.size
theorem Array.extract_extract {α : Type u} {s1 : Nat} {e2 : Nat} {e1 : Nat} {s2 : Nat} {a : Array α} (h : s1 + e2 e1) :
(a.extract s1 e1).extract s2 e2 = a.extract (s1 + s2) (s1 + e2)