Lemmas about Vector.extract

extract

@[simp]

theorem Vector.extract_of_size_lt {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (h : n < j) : xs.extract i j = Vector.cast ⋯ (xs.extract i)

@[simp]

theorem Vector.extract_push {α : Type u_1} {n : Nat} {xs : Vector α n} {b : α} {start stop : Nat} (h : stop ≤ n) : (xs.push b).extract start stop = Vector.cast ⋯ (xs.extract start stop)

@[simp]

theorem Vector.extract_eq_pop {α : Type u_1} {n : Nat} {xs : Vector α n} {stop : Nat} (h : stop = n - 1) : xs.extract 0 stop = Vector.cast ⋯ xs.pop

@[simp]

theorem Vector.extract_append_extract {α : Type u_1} {n : Nat} {xs : Vector α n} {i j k : Nat} : xs.extract i j ++ xs.extract j k = Vector.cast ⋯ (xs.extract (min i j) (max j k))

@[simp]

theorem Vector.push_extract_getElem {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (h : j < n) : (xs.extract i j).push xs[j] = Vector.cast ⋯ (xs.extract (min i j) (j + 1))

theorem Vector.extract_succ_right {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (w : i < j + 1) (h : j < n) : xs.extract i (j + 1) = Vector.cast ⋯ ((xs.extract i j).push xs[j])

theorem Vector.extract_sub_one {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (h : j < n) : xs.extract i (j - 1) = Vector.cast ⋯ (xs.extract i j).pop

@[simp]

theorem Vector.getElem?_extract_of_lt {α : Type u_1} {n : Nat} {xs : Vector α n} {i j k : Nat} (h : k < min j n - i) : (xs.extract i j)[k]? = some xs[i + k]

theorem Vector.getElem?_extract_of_succ {α : Type u_1} {n : Nat} {xs : Vector α n} {j : Nat} : (xs.extract 0 (j + 1))[j]? = xs[j]?

@[simp]

theorem Vector.extract_extract {α : Type u_1} {n : Nat} {xs : Vector α n} {i j k l : Nat} : (xs.extract i j).extract k l = Vector.cast ⋯ (xs.extract (i + k) (min (i + l) j))

theorem Vector.extract_set {α : Type u_1} {n : Nat} {xs : Vector α n} {i j k : Nat} (h : k < n) {a : α} : (xs.set k a h).extract i j = if x : k < i then xs.extract i j else if x_1 : k < min j xs.size then (xs.extract i j).set (k - i) a ⋯ else xs.extract i j

theorem Vector.set_extract {α : Type u_1} {n : Nat} {xs : Vector α n} {i j k : Nat} (h : k < min j n - i) {a : α} : (xs.extract i j).set k a h = (xs.set (i + k) a ⋯).extract i j

@[simp]

theorem Vector.extract_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i j : Nat} : (xs ++ ys).extract i j = Vector.cast ⋯ (xs.extract i j ++ ys.extract (i - n) (j - n))

theorem Vector.extract_append_left {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).extract 0 n = Vector.cast ⋯ xs.extract

@[simp]

theorem Vector.extract_append_right {α : Type u_1} {n m i : Nat} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).extract n (n + i) = Vector.cast ⋯ (ys.extract 0 i)

@[simp]

theorem Vector.map_extract {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : α → α✝} {xs : Vector α n} {i j : Nat} : map f (xs.extract i j) = (map f xs).extract i j

@[simp]

theorem Vector.extract_mkVector {α : Type u_1} {a : α} {n i j : Nat} : (mkVector n a).extract i j = mkVector (min j n - i) a

theorem Vector.extract_add_left {α : Type u_1} {n : Nat} {xs : Vector α n} {i j k : Nat} : xs.extract (i + j) k = Vector.cast ⋯ ((xs.extract i k).extract j (k - i))

theorem Vector.mem_extract_iff_getElem {α : Type u_1} {n : Nat} {xs : Vector α n} {a : α} {i j : Nat} : a ∈ xs.extract i j ↔ ∃ (k : Nat), ∃ (hm : k < min j n - i), xs[i + k] = a

theorem Vector.set_eq_push_extract_append_extract {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) {a : α} : xs.set i a h = Vector.cast ⋯ ((xs.extract 0 i).push a ++ xs.extract (i + 1))

theorem Vector.extract_reverse {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} : xs.reverse.extract i j = Vector.cast ⋯ (xs.extract (n - j) (n - i)).reverse

theorem Vector.reverse_extract {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} : (xs.extract i j).reverse = Vector.cast ⋯ (xs.reverse.extract (n - j) (n - i))