theorem Vector.toArray_injective {α : Type u_1} {n : Nat} {v w : Vector α n} : v.toArray = w.toArray → v = w

mk lemmas

@[simp]

theorem Vector.get_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) : { toArray := a, size_toArray := h }.get i = a[i]

@[simp]

theorem Vector.getD_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : { toArray := a, size_toArray := h }.getD i x = a.getD i x

@[simp]

theorem Vector.uget_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : USize) (hi : i.toNat < n) : { toArray := a, size_toArray := h }.uget i hi = a.uget i ⋯

@[deprecated Vector.set_mk (since := "2024-11-25")]

theorem Vector.setN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (w : i < n) : { toArray := a, size_toArray := h }.set i x w = { toArray := a.set i x ⋯, size_toArray := ⋯ }

Alias of Vector.set_mk.

@[deprecated Vector.swap_mk (since := "2024-11-25")]

theorem Vector.swapN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) (hi : j < n) (hj : i < n) : { toArray := a, size_toArray := h }.swap i j hj hi = { toArray := a.swap i j ⋯ ⋯, size_toArray := ⋯ }

Alias of Vector.swap_mk.

@[deprecated Vector.swapAt_mk (since := "2024-11-25")]

theorem Vector.swapAtN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (hi : i < n) : { toArray := a, size_toArray := h }.swapAt i x hi = ((a.swapAt i x ⋯).fst, { toArray := (a.swapAt i x ⋯).snd, size_toArray := ⋯ })

Alias of Vector.swapAt_mk.

toArray lemmas

@[deprecated Vector.toArray_setIfInBounds (since := "2024-11-25")]

theorem Vector.toArray_setD {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) : (a.setIfInBounds i x).toArray = a.setIfInBounds i x

Alias of Vector.toArray_setIfInBounds.

@[deprecated Vector.toArray_set (since := "2024-11-25")]

theorem Vector.toArray_setN {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) : (a.set i x h).toArray = a.set i x ⋯

Alias of Vector.toArray_set.

@[deprecated Vector.toArray_swapIfInBounds (since := "2024-11-25")]

theorem Vector.toArray_swap! {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) : (a.swapIfInBounds i j).toArray = a.swapIfInBounds i j

Alias of Vector.toArray_swapIfInBounds.

@[deprecated Vector.toArray_swap (since := "2024-11-25")]

theorem Vector.toArray_swapN {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) (hi : j < n) (hj : i < n) : (a.swap i j hj hi).toArray = a.swap i j ⋯ ⋯

Alias of Vector.toArray_swap.

@[deprecated Vector.toArray_swapAt (since := "2024-11-25")]

theorem Vector.toArray_swapAtN {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) : ((a.swapAt i x h).fst, (a.swapAt i x h).snd.toArray) = ((a.swapAt i x ⋯).fst, (a.swapAt i x ⋯).snd)

Alias of Vector.toArray_swapAt.