Lemmas about Array.extract

Some useful lemmas about Array.extract

@[deprecated Array.extract_empty_of_start_eq_stop (since := "2025-11-03")]

theorem Array.extract_eq_nil_of_start_eq_end {α : Type u_1} {i : ℕ} {a : Array α} : a.extract i i = #[]

Alias of Array.extract_empty_of_start_eq_stop.

@[deprecated Array.extract_append_of_stop_le_size_left (since := "2025-11-03")]

theorem Array.extract_append_left' {α : Type u_1} {j i : ℕ} {a b : Array α} (h : j ≤ a.size) : (a ++ b).extract i j = a.extract i j

Alias of Array.extract_append_of_stop_le_size_left.

@[deprecated Array.extract_append_of_size_left_le_start (since := "2025-11-03")]

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

Alias of Array.extract_append_of_size_left_le_start.

@[deprecated Array.extract_eq_of_size_le_stop (since := "2025-11-03")]

theorem Array.extract_eq_of_size_le_end {α : Type u_1} {j i : ℕ} {a : Array α} (h : a.size ≤ j) : a.extract i j = a.extract i

Alias of Array.extract_eq_of_size_le_stop.