Documentation

Mathlib.Data.Array.Extract

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 b : Array α} {i j : Nat} (h : j a.size) :
(a ++ b).extract i j = a.extract i j

This is a stronger version of Array.extract_append_left, and should be upstreamed to replace that.

theorem Array.extract_append_right' {α : Type u} {a b : Array α} {i j : Nat} (h : a.size i) :
(a ++ b).extract i j = b.extract (i - a.size) (j - a.size)

This is a stronger version of Array.extract_append_right, and should be upstreamed to replace that.

theorem Array.extract_eq_of_size_le_end {α : Type u} {l p : Nat} {a : Array α} (h : a.size l) :
a.extract p l = a.extract p