Lemmas about Array.extract #
Some useful lemmas about Array.extract
@[simp]
theorem
Array.extract_eq_nil_of_start_eq_end
{α : Type u_1}
{i : Nat}
{a : Array α}
:
Array.extract a i i = #[]
theorem
Array.extract_append_left
{α : Type u_1}
{a : Array α}
{b : Array α}
{i : Nat}
{j : Nat}
(h : j ≤ Array.size a)
:
Array.extract (a ++ b) i j = Array.extract a i j
theorem
Array.extract_append_right
{α : Type u_1}
{a : Array α}
{b : Array α}
{i : Nat}
{j : Nat}
(h : i ≥ Array.size a)
:
Array.extract (a ++ b) i j = Array.extract b (i - Array.size a) (j - Array.size a)
theorem
Array.extract_eq_of_size_le_end
{α : Type u_1}
{l : Nat}
{p : Nat}
{a : Array α}
:
Array.size a ≤ l → Array.extract a p l = Array.extract a p (Array.size a)
theorem
Array.extract_extract
{α : Type u_1}
{s1 : Nat}
{e2 : Nat}
{e1 : Nat}
{s2 : Nat}
{a : Array α}
(h : s1 + e2 ≤ e1)
:
Array.extract (Array.extract a s1 e1) s2 e2 = Array.extract a (s1 + s2) (s1 + e2)