Vectors

Lemmas about Vector α n

theorem Array.toVector_inj {α : Type u_1} {xs ys : Array α} (h₁ : xs.size = ys.size) (h₂ : Vector.cast h₁ xs.toVector = ys.toVector) : xs = ys

mk lemmas

theorem Vector.toArray_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) : (mk xs h).toArray = xs

@[simp]

theorem Vector.mk_toArray {α : Type u_1} {n : Nat} {xs : Vector α n} : mk xs.toArray ⋯ = xs

@[simp]

theorem Vector.getElem_mk {α : Type u_1} {n : Nat} {xs : Array α} {size : xs.size = n} {i : Nat} (h : i < n) : (mk xs size)[i] = xs[i]

@[simp]

theorem Vector.getElem?_mk {α : Type u_1} {n : Nat} {xs : Array α} {size : xs.size = n} {i : Nat} : (mk xs size)[i]? = xs[i]?

@[simp]

theorem Vector.mem_mk {α : Type u_1} {n : Nat} {xs : Array α} {size : xs.size = n} {a : α} : a ∈ mk xs size ↔ a ∈ xs

@[simp]

theorem Vector.contains_mk {α : Type u_1} {n : Nat} [BEq α] {xs : Array α} {size : xs.size = n} {a : α} : (mk xs size).contains a = xs.contains a

@[simp]

theorem Vector.push_mk {α : Type u_1} {n : Nat} {xs : Array α} {size : xs.size = n} : (mk xs size).push = fun (x : α) => mk (xs.push x) ⋯

@[simp]

theorem Vector.pop_mk {α : Type u_1} {n : Nat} {xs : Array α} {size : xs.size = n} : (mk xs size).pop = mk xs.pop ⋯

@[simp]

theorem Vector.mk_beq_mk {α : Type u_1} {n : Nat} [BEq α] {xs ys : Array α} {h : xs.size = n} {h' : ys.size = n} : (mk xs h == mk ys h') = (xs == ys)

@[simp]

theorem Vector.mk_append_mk {α : Type u_1} {n m : Nat} {xs ys : Array α} (h : xs.size = n) (h' : ys.size = m) : mk xs h ++ mk ys h' = mk (xs ++ ys) ⋯

@[simp]

theorem Vector.back!_mk {α : Type u_1} {n : Nat} [Inhabited α] {xs : Array α} (h : xs.size = n) : (mk xs h).back! = xs.back!

@[simp]

theorem Vector.back?_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) : (mk xs h).back? = xs.back?

@[simp]

theorem Vector.back_mk {n : Nat} {α : Type u_1} [NeZero n] {xs : Array α} (h : xs.size = n) : (mk xs h).back = xs.back ⋯

@[simp]

theorem Vector.foldlM_mk {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} [Monad m] {f : β → α → m β} {b : β} {xs : Array α} (h : xs.size = n) : foldlM f b (mk xs h) = Array.foldlM f b xs

@[simp]

theorem Vector.foldrM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] {f : α → β → m β} {b : β} {xs : Array α} (h : xs.size = n) : foldrM f b (mk xs h) = Array.foldrM f b xs

@[simp]

theorem Vector.foldl_mk {β : Type u_1} {α : Type u_2} {n : Nat} {f : β → α → β} {b : β} {xs : Array α} (h : xs.size = n) : foldl f b (mk xs h) = Array.foldl f b xs

@[simp]

theorem Vector.foldr_mk {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β → β} {b : β} {xs : Array α} (h : xs.size = n) : foldr f b (mk xs h) = Array.foldr f b xs

@[simp]

theorem Vector.drop_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {i : Nat} : (mk xs h).drop i = mk (xs.extract i) ⋯

@[simp]

theorem Vector.eraseIdx_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {i : Nat} (h' : i < n) : (mk xs h).eraseIdx i h' = mk (xs.eraseIdx i ⋯) ⋯

@[simp]

theorem Vector.eraseIdx!_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {i : Nat} (hi : i < n) : (mk xs h).eraseIdx! i = mk (xs.eraseIdx i ⋯) ⋯

@[simp]

theorem Vector.insertIdx_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {i : Nat} {x : α} (h' : i ≤ n) : (mk xs h).insertIdx i x h' = mk (xs.insertIdx i x ⋯) ⋯

@[simp]

theorem Vector.insertIdx!_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {i : Nat} {x : α} (hi : i ≤ n) : (mk xs h).insertIdx! i x = mk (xs.insertIdx i x ⋯) ⋯

@[simp]

theorem Vector.cast_mk {α : Type u_1} {n m : Nat} {xs : Array α} {h : xs.size = n} {h' : n = m} : Vector.cast h' (mk xs h) = mk xs ⋯

@[simp]

theorem Vector.extract_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {start stop : Nat} : (mk xs h).extract start stop = mk (xs.extract start stop) ⋯

@[simp]

theorem Vector.finIdxOf?_mk {α : Type u_1} {n : Nat} [BEq α] {xs : Array α} (h : xs.size = n) (x : α) : (mk xs h).finIdxOf? x = Option.map (Fin.cast h) (xs.finIdxOf? x)

@[simp]

theorem Vector.findFinIdx?_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) (f : α → Bool) : findFinIdx? f (mk xs h) = Option.map (Fin.cast h) (Array.findFinIdx? f xs)

@[simp]

theorem Vector.findM?_mk {m : Type → Type} {α : Type} {n : Nat} [Monad m] {xs : Array α} (h : xs.size = n) (f : α → m Bool) : findM? f (mk xs h) = Array.findM? f xs

@[simp]

theorem Vector.findSomeM?_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] {xs : Array α} (h : xs.size = n) (f : α → m (Option β)) : findSomeM? f (mk xs h) = Array.findSomeM? f xs

@[simp]

theorem Vector.findRevM?_mk {m : Type → Type} {α : Type} {n : Nat} [Monad m] {xs : Array α} (h : xs.size = n) (f : α → m Bool) : findRevM? f (mk xs h) = Array.findRevM? f xs

@[simp]

theorem Vector.findSomeRevM?_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] {xs : Array α} (h : xs.size = n) (f : α → m (Option β)) : findSomeRevM? f (mk xs h) = Array.findSomeRevM? f xs

@[simp]

theorem Vector.find?_mk {α : Type} {n : Nat} {xs : Array α} (h : xs.size = n) (f : α → Bool) : find? f (mk xs h) = Array.find? f xs

@[simp]

theorem Vector.findSome?_mk {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Array α} (h : xs.size = n) (f : α → Option β) : findSome? f (mk xs h) = Array.findSome? f xs

@[simp]

theorem Vector.findRev?_mk {α : Type} {n : Nat} {xs : Array α} (h : xs.size = n) (f : α → Bool) : findRev? f (mk xs h) = Array.findRev? f xs

@[simp]

theorem Vector.findSomeRev?_mk {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Array α} (h : xs.size = n) (f : α → Option β) : findSomeRev? f (mk xs h) = Array.findSomeRev? f xs

@[simp]

theorem Vector.mk_isEqv_mk {α : Type u_1} {n : Nat} {r : α → α → Bool} {xs ys : Array α} (h : xs.size = n) (h' : ys.size = n) : (mk xs h).isEqv (mk ys h') r = xs.isEqv ys r

@[simp]

theorem Vector.mk_isPrefixOf_mk {α : Type u_1} {n : Nat} [BEq α] {xs ys : Array α} (h : xs.size = n) (h' : ys.size = n) : (mk xs h).isPrefixOf (mk ys h') = xs.isPrefixOf ys

@[simp]

theorem Vector.map_mk {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Array α} (h : xs.size = n) : map f (mk xs h) = mk (Array.map f xs) ⋯

@[simp]

theorem Vector.mapIdx_mk {α : Type u_1} {β : Type u_2} {n : Nat} {f : Nat → α → β} {xs : Array α} (h : xs.size = n) : mapIdx f (mk xs h) = mk (Array.mapIdx f xs) ⋯

@[simp]

theorem Vector.mapFinIdx_mk {α : Type u_1} {n : Nat} {β : Type u_2} {f : (i : Nat) → α → i < n → β} {xs : Array α} (h : xs.size = n) : (mk xs h).mapFinIdx f = mk (xs.mapFinIdx fun (i : Nat) (a : α) (h' : i < xs.size) => f i a ⋯) ⋯

@[simp]

theorem Vector.forM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} [Monad m] {f : α → m PUnit} {xs : Array α} (h : xs.size = n) : forM (mk xs h) f = forM xs f

@[simp]

theorem Vector.forIn'_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] {xs : Array α} (h : xs.size = n) {b : β} {f : (a : α) → a ∈ mk xs h → β → m (ForInStep β)} : forIn' (mk xs h) b f = forIn' xs b fun (a : α) (m : a ∈ xs) (b : β) => f a ⋯ b

@[simp]

theorem Vector.forIn_mk {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] {f : α → β → m (ForInStep β)} {xs : Array α} (h : xs.size = n) {b : β} : forIn (mk xs h) b f = forIn xs b f

@[simp]

theorem Vector.flatMap_mk {α : Type u_1} {β : Type u_2} {m n : Nat} {f : α → Vector β m} {xs : Array α} (h : xs.size = n) : (mk xs h).flatMap f = mk (Array.flatMap (fun (a : α) => (f a).toArray) xs) ⋯

@[simp]

theorem Vector.firstM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Alternative m] {f : α → m β} {xs : Array α} (h : xs.size = n) : firstM f (mk xs h) = Array.firstM f xs

@[simp]

theorem Vector.reverse_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) : (mk xs h).reverse = mk xs.reverse ⋯

@[simp]

theorem Vector.set_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i : Nat} {x : α} (w : i < n) : (mk xs h).set i x w = mk (xs.set i x ⋯) ⋯

@[simp]

theorem Vector.set!_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i : Nat} {x : α} : (mk xs h).set! i x = mk (xs.set! i x) ⋯

@[simp]

theorem Vector.setIfInBounds_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i : Nat} {x : α} : (mk xs h).setIfInBounds i x = mk (xs.setIfInBounds i x) ⋯

@[simp]

theorem Vector.swap_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i j : Nat} (hi : j < n) (hj : i < n) : (mk xs h).swap i j hj hi = mk (xs.swap i j ⋯ ⋯) ⋯

@[simp]

theorem Vector.swapIfInBounds_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i j : Nat} : (mk xs h).swapIfInBounds i j = mk (xs.swapIfInBounds i j) ⋯

@[simp]

theorem Vector.swapAt_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i : Nat} {x : α} (hi : i < n) : (mk xs h).swapAt i x hi = ((xs.swapAt i x ⋯).fst, mk (xs.swapAt i x ⋯).snd ⋯)

@[simp]

theorem Vector.swapAt!_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i : Nat} {x : α} : (mk xs h).swapAt! i x = ((xs.swapAt! i x).fst, mk (xs.swapAt! i x).snd ⋯)

@[simp]

theorem Vector.take_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) {i : Nat} : (mk xs h).take i = mk (xs.take i) ⋯

@[simp]

theorem Vector.zipIdx_mk {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n) (k : Nat := 0) : (mk xs h).zipIdx k = mk (xs.zipIdx k) ⋯

@[simp]

theorem Vector.mk_zipWith_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β → γ} {as : Array α} {bs : Array β} (h : as.size = n) (h' : bs.size = n) : zipWith f (mk as h) (mk bs h') = mk (Array.zipWith f as bs) ⋯

@[simp]

theorem Vector.mk_zip_mk {α : Type u_1} {β : Type u_2} {n : Nat} {as : Array α} {bs : Array β} (h : as.size = n) (h' : bs.size = n) : (mk as h).zip (mk bs h') = mk (as.zip bs) ⋯

@[simp]

theorem Vector.unzip_mk {α : Type u_1} {β : Type u_2} {n : Nat} {xs : Array (α × β)} (h : xs.size = n) : (mk xs h).unzip = (mk xs.unzip.fst ⋯, mk xs.unzip.snd ⋯)

@[simp]

theorem Vector.anyM_mk {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] {p : α → m Bool} {xs : Array α} (h : xs.size = n) : anyM p (mk xs h) = Array.anyM p xs

@[simp]

theorem Vector.allM_mk {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] {p : α → m Bool} {xs : Array α} (h : xs.size = n) : allM p (mk xs h) = Array.allM p xs

@[simp]

theorem Vector.any_mk {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Array α} (h : xs.size = n) : (mk xs h).any p = xs.any p

@[simp]

theorem Vector.all_mk {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Array α} (h : xs.size = n) : (mk xs h).all p = xs.all p

@[simp]

theorem Vector.countP_mk {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Array α} (h : xs.size = n) : countP p (mk xs h) = Array.countP p xs

@[simp]

theorem Vector.count_mk {α : Type u_1} {n : Nat} [BEq α] {xs : Array α} (h : xs.size = n) {a : α} : count a (mk xs h) = Array.count a xs

@[simp]

theorem Vector.replace_mk {α : Type u_1} {n : Nat} [BEq α] {xs : Array α} (h : xs.size = n) {a b : α} : (mk xs h).replace a b = mk (xs.replace a b) ⋯

@[simp]

theorem Vector.sum_mk {α : Type u_1} {n : Nat} [Add α] [Zero α] {xs : Array α} (h : xs.size = n) : (mk xs h).sum = xs.sum

@[simp]

theorem Vector.sum_toArray {α : Type u_1} {n : Nat} [Add α] [Zero α] {xs : Vector α n} : xs.toArray.sum = xs.sum

@[simp]

theorem Vector.eq_mk {α✝ : Type u_1} {n✝ : Nat} {xs : Vector α✝ n✝} {as : Array α✝} {h : as.size = n✝} : xs = mk as h ↔ xs.toArray = as

@[simp]

theorem Vector.mk_eq {α✝ : Type u_1} {as : Array α✝} {a✝ : Nat} {h : as.size = a✝} {xs : Vector α✝ a✝} : mk as h = xs ↔ as = xs.toArray

toArray lemmas

@[simp]

theorem Vector.getElem_toArray {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < xs.toArray.size) : xs.toArray[i] = xs[i]

@[simp]

theorem Vector.getElem?_toArray {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : xs.toArray[i]? = xs[i]?

@[simp]

theorem Vector.toArray_append {α : Type u_1} {m n : Nat} {xs : Vector α m} {ys : Vector α n} : (xs ++ ys).toArray = xs.toArray ++ ys.toArray

@[simp]

theorem Vector.toArray_drop {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : (xs.drop i).toArray = xs.toArray.extract i n

@[simp]

theorem Vector.toArray_empty {α : Type u_1} : #v[].toArray = #[]

@[simp]

theorem Vector.toArray_emptyWithCapacity {α : Type u_1} {cap : Nat} : (emptyWithCapacity cap).toArray = Array.emptyWithCapacity cap

@[simp]

theorem Vector.toArray_eraseIdx {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : (xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i ⋯

@[simp]

theorem Vector.toArray_eraseIdx! {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (hi : i < n) : (xs.eraseIdx! i).toArray = xs.toArray.eraseIdx! i

@[simp]

theorem Vector.toArray_insertIdx {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} (h : i ≤ n) : (xs.insertIdx i x h).toArray = xs.toArray.insertIdx i x ⋯

@[simp]

theorem Vector.toArray_insertIdx! {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} (hi : i ≤ n) : (xs.insertIdx! i x).toArray = xs.toArray.insertIdx! i x

@[simp]

theorem Vector.toArray_cast {α : Type u_1} {n m : Nat} {xs : Vector α n} (h : n = m) : (Vector.cast h xs).toArray = xs.toArray

@[simp]

theorem Vector.toArray_extract {α : Type u_1} {n : Nat} {xs : Vector α n} {start stop : Nat} : (xs.extract start stop).toArray = xs.toArray.extract start stop

@[simp]

theorem Vector.toArray_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} : (map f xs).toArray = Array.map f xs.toArray

@[simp]

theorem Vector.toArray_mapIdx {α : Type u_1} {β : Type u_2} {n : Nat} {f : Nat → α → β} {xs : Vector α n} : (mapIdx f xs).toArray = Array.mapIdx f xs.toArray

@[simp]

theorem Vector.toArray_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} {f : (i : Nat) → α → i < n → β} {xs : Vector α n} : (xs.mapFinIdx f).toArray = xs.toArray.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.toArray.size) => f i a ⋯

@[simp]

theorem Vector.toArray_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} : toArray <$> mapM f xs = Array.mapM f xs.toArray

@[simp]

theorem Vector.toArray_ofFn {n : Nat} {α : Type u_1} {f : Fin n → α} : (ofFn f).toArray = Array.ofFn f

@[simp]

theorem Vector.toArray_pop {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.pop.toArray = xs.toArray.pop

@[simp]

theorem Vector.toArray_push {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} : (xs.push x).toArray = xs.toArray.push x

@[simp]

theorem Vector.toArray_beq_toArray {α : Type u_1} {n : Nat} [BEq α] {xs ys : Vector α n} : (xs.toArray == ys.toArray) = (xs == ys)

@[simp]

theorem Vector.toArray_range {n : Nat} : (range n).toArray = Array.range n

@[simp]

theorem Vector.toArray_reverse {α : Type u_1} {n : Nat} (xs : Vector α n) : xs.reverse.toArray = xs.toArray.reverse

@[simp]

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

@[simp]

theorem Vector.toArray_set! {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} : (xs.set! i x).toArray = xs.toArray.set! i x

@[simp]

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

@[simp]

theorem Vector.toArray_singleton {α : Type u_1} {x : α} : (singleton x).toArray = #[x]

@[simp]

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

@[simp]

theorem Vector.toArray_swapIfInBounds {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} : (xs.swapIfInBounds i j).toArray = xs.toArray.swapIfInBounds i j

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

theorem Vector.toArray_swapAt! {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} : ((xs.swapAt! i x).fst, (xs.swapAt! i x).snd.toArray) = ((xs.toArray.swapAt! i x).fst, (xs.toArray.swapAt! i x).snd)

@[simp]

theorem Vector.toArray_take {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : (xs.take i).toArray = xs.toArray.take i

@[simp]

theorem Vector.toArray_zipIdx {α : Type u_1} {n : Nat} {xs : Vector α n} (k : Nat := 0) : (xs.zipIdx k).toArray = xs.toArray.zipIdx k

@[simp]

theorem Vector.toArray_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β → γ} {as : Vector α n} {bs : Vector β n} : (zipWith f as bs).toArray = Array.zipWith f as.toArray bs.toArray

@[simp]

theorem Vector.anyM_toArray {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] {p : α → m Bool} {xs : Vector α n} : Array.anyM p xs.toArray = anyM p xs

@[simp]

theorem Vector.allM_toArray {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] {p : α → m Bool} {xs : Vector α n} : Array.allM p xs.toArray = allM p xs

@[simp]

theorem Vector.any_toArray {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.toArray.any p = xs.any p

@[simp]

theorem Vector.all_toArray {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.toArray.all p = xs.all p

@[simp]

theorem Vector.countP_toArray {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : Array.countP p xs.toArray = countP p xs

@[simp]

theorem Vector.count_toArray {α : Type u_1} {n : Nat} [BEq α] {a : α} {xs : Vector α n} : Array.count a xs.toArray = count a xs

@[simp]

theorem Vector.replace_toArray {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {a b : α} : xs.toArray.replace a b = (xs.replace a b).toArray

@[simp]

theorem Vector.find?_toArray {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} : Array.find? p xs.toArray = find? p xs

@[simp]

theorem Vector.findSome?_toArray {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} : Array.findSome? f xs.toArray = findSome? f xs

@[simp]

theorem Vector.findRev?_toArray {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} : Array.findRev? p xs.toArray = findRev? p xs

@[simp]

theorem Vector.findSomeRev?_toArray {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} : Array.findSomeRev? f xs.toArray = findSomeRev? f xs

@[simp]

theorem Vector.findM?_toArray {m : Type → Type} {α : Type} {n : Nat} [Monad m] {p : α → m Bool} {xs : Vector α n} : Array.findM? p xs.toArray = findM? p xs

@[simp]

theorem Vector.findSomeM?_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] {f : α → m (Option β)} {xs : Vector α n} : Array.findSomeM? f xs.toArray = findSomeM? f xs

@[simp]

theorem Vector.findRevM?_toArray {m : Type → Type} {α : Type} {n : Nat} [Monad m] {p : α → m Bool} {xs : Vector α n} : Array.findRevM? p xs.toArray = findRevM? p xs

@[simp]

theorem Vector.findSomeRevM?_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] {f : α → m (Option β)} {xs : Vector α n} : Array.findSomeRevM? f xs.toArray = findSomeRevM? f xs

@[simp]

theorem Vector.finIdxOf?_toArray {α : Type u_1} {n : Nat} [BEq α] {a : α} {xs : Vector α n} : xs.toArray.finIdxOf? a = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)

@[simp]

theorem Vector.findFinIdx?_toArray {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : Array.findFinIdx? p xs.toArray = Option.map (Fin.cast ⋯) (findFinIdx? p xs)

@[simp]

theorem Vector.toArray_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} : (replicate n a).toArray = Array.replicate n a

@[simp]

theorem Vector.toArray_inj {α : Type u_1} {n : Nat} {xs ys : Vector α n} : xs.toArray = ys.toArray ↔ xs = ys

theorem Vector.ext {α : Type u_1} {n : Nat} {xs ys : Vector α n} (h : ∀ (i : Nat) (x : i < n), xs[i] = ys[i]) : xs = ys

Vector.ext is an extensionality theorem. Vectors a and b are equal to each other if their elements are equal for each valid index.

theorem Vector.ext_iff {α : Type u_1} {n : Nat} {xs ys : Vector α n} : xs = ys ↔ ∀ (i : Nat) (x : i < n), xs[i] = ys[i]

@[simp]

theorem Vector.toArray_eq_empty_iff {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.toArray = #[] ↔ n = 0

toList

@[simp]

theorem Vector.length_toList {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.toList.length = n

theorem Vector.toList_toArray {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.toArray.toList = xs.toList

@[simp]

theorem Vector.toList_mk {α✝ : Type u_1} {xs : Array α✝} {a✝ : Nat} {h : xs.size = a✝} : (mk xs h).toList = xs.toList

@[simp]

theorem Vector.sum_toList {α : Type u_1} {n : Nat} [Add α] [Zero α] {xs : Vector α n} : xs.toList.sum = xs.sum

@[simp]

theorem Vector.toList_zip {α : Type u_1} {n : Nat} {β : Type u_2} {as : Vector α n} {bs : Vector β n} : (as.zip bs).toList = as.toList.zip bs.toList

@[simp]

theorem Vector.getElem_toList {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) : xs.toList[i] = xs[i]

@[simp]

theorem Vector.getElem?_toList {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : xs.toList[i]? = xs[i]?

@[simp]

theorem Vector.toList_append {α : Type u_1} {m n : Nat} {xs : Vector α m} {ys : Vector α n} : (xs ++ ys).toList = xs.toList ++ ys.toList

@[simp]

theorem Vector.toList_drop {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : (xs.drop i).toList = List.drop i xs.toList

theorem Vector.toList_empty {α : Type u_1} : #v[].toList = []

theorem Vector.toList_emptyWithCapacity {α : Type u_1} {cap : Nat} : (emptyWithCapacity cap).toList = []

theorem Vector.toList_eraseIdx {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : (xs.eraseIdx i h).toList = xs.toList.eraseIdx i

@[simp]

theorem Vector.toList_eraseIdx! {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (hi : i < n) : (xs.eraseIdx! i).toList = xs.toList.eraseIdx i

theorem Vector.toList_insertIdx {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} (h : i ≤ n) : (xs.insertIdx i x h).toList = xs.toList.insertIdx i x

theorem Vector.toList_insertIdx! {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} (hi : i ≤ n) : (xs.insertIdx! i x).toList = xs.toList.insertIdx i x

theorem Vector.toList_cast {α : Type u_1} {n m : Nat} {xs : Vector α n} (h : n = m) : (Vector.cast h xs).toList = xs.toList

theorem Vector.toList_extract {α : Type u_1} {n : Nat} {xs : Vector α n} {start stop : Nat} : (xs.extract start stop).toList = List.take (stop - start) (List.drop start xs.toList)

theorem Vector.toList_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} : (map f xs).toList = List.map f xs.toList

theorem Vector.toList_mapIdx {α : Type u_1} {β : Type u_2} {n : Nat} {f : Nat → α → β} {xs : Vector α n} : (mapIdx f xs).toList = List.mapIdx f xs.toList

theorem Vector.toList_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} {f : (i : Nat) → α → i < n → β} {xs : Vector α n} : (xs.mapFinIdx f).toList = xs.toList.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.toList.length) => f i a ⋯

theorem Vector.toList_ofFn {n : Nat} {α : Type u_1} {f : Fin n → α} : (ofFn f).toList = List.ofFn f

theorem Vector.toList_pop {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.pop.toList = xs.toList.dropLast

theorem Vector.toList_push {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} : (xs.push x).toList = xs.toList ++ [x]

@[simp]

theorem Vector.toList_beq_toList {α : Type u_1} {n : Nat} [BEq α] {xs ys : Vector α n} : (xs.toList == ys.toList) = (xs == ys)

theorem Vector.toList_range {n : Nat} : (range n).toList = List.range n

@[simp]

theorem Vector.toList_reverse {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.reverse.toList = xs.toList.reverse

theorem Vector.toList_set {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} (h : i < n) : (xs.set i x h).toList = xs.toList.set i x

@[simp]

theorem Vector.toList_setIfInBounds {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} : (xs.setIfInBounds i x).toList = xs.toList.set i x

theorem Vector.toList_singleton {α : Type u_1} {x : α} : (singleton x).toList = [x]

theorem Vector.toList_swap {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (hi : j < n) (hj : i < n) : (xs.swap i j hj hi).toList = (xs.toList.set i xs[j]).set j xs[i]

@[simp]

theorem Vector.toList_take {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : (xs.take i).toList = List.take i xs.toList

@[simp]

theorem Vector.toList_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β → γ} {as : Vector α n} {bs : Vector β n} : (zipWith f as bs).toList = List.zipWith f as.toList bs.toList

@[simp]

theorem Vector.anyM_toList {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] {p : α → m Bool} {xs : Vector α n} : List.anyM p xs.toList = anyM p xs

@[simp]

theorem Vector.allM_toList {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n} : List.allM p xs.toList = allM p xs

@[simp]

theorem Vector.any_toList {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.toList.any p = xs.any p

@[simp]

theorem Vector.all_toList {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.toList.all p = xs.all p

@[simp]

theorem Vector.countP_toList {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : List.countP p xs.toList = countP p xs

@[simp]

theorem Vector.count_toList {α : Type u_1} {n : Nat} [BEq α] {a : α} {xs : Vector α n} : List.count a xs.toList = count a xs

@[simp]

theorem Vector.find?_toList {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} : List.find? p xs.toList = find? p xs

@[simp]

theorem Vector.findSome?_toList {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} : List.findSome? f xs.toList = findSome? f xs

@[simp]

theorem Vector.findM?_toList {m : Type → Type} {α : Type} {n : Nat} [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n} : List.findM? p xs.toList = findM? p xs

@[simp]

theorem Vector.findSomeM?_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : α → m (Option β)} {xs : Vector α n} : List.findSomeM? f xs.toList = findSomeM? f xs

@[simp]

theorem Vector.finIdxOf?_toList {α : Type u_1} {n : Nat} [BEq α] {a : α} {xs : Vector α n} : List.finIdxOf? a xs.toList = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)

@[simp]

theorem Vector.findFinIdx?_toList {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : List.findFinIdx? p xs.toList = Option.map (Fin.cast ⋯) (findFinIdx? p xs)

@[simp]

theorem Vector.toList_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} : (replicate n a).toList = List.replicate n a

theorem Vector.toList_inj {α : Type u_1} {n : Nat} {xs ys : Vector α n} : xs.toList = ys.toList ↔ xs = ys

@[simp]

theorem Vector.toList_eq_nil_iff {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.toList = [] ↔ n = 0

@[simp]

theorem Vector.mem_toList_iff {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : a ∈ xs.toList ↔ a ∈ xs

empty

theorem Vector.empty_eq {α : Type u_1} {xs : Vector α 0} : #v[] = xs ↔ xs = #v[]

theorem Vector.eq_empty {α : Type u_1} {xs : Vector α 0} : xs = #v[]

A vector of length 0 is the empty vector.

size

theorem Vector.eq_empty_of_size_eq_zero {α : Type u_1} {n : Nat} {xs : Vector α n} (h : n = 0) : xs = Vector.cast ⋯ #v[]

theorem Vector.size_eq_one {α : Type u_1} {xs : Vector α 1} : ∃ (a : α), xs = #v[a]

push

theorem Vector.back_eq_of_push_eq {α : Type u_1} {n : Nat} {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : a = b

theorem Vector.pop_eq_of_push_eq {α : Type u_1} {n : Nat} {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : xs = ys

theorem Vector.push_inj_left {α : Type u_1} {n : Nat} {a : α} {xs ys : Vector α n} : xs.push a = ys.push a ↔ xs = ys

theorem Vector.push_inj_right {α : Type u_1} {n : Nat} {a b : α} {xs : Vector α n} : xs.push a = xs.push b ↔ a = b

theorem Vector.push_eq_push {α : Type u_1} {n : Nat} {a b : α} {xs ys : Vector α n} : xs.push a = ys.push b ↔ a = b ∧ xs = ys

theorem Vector.exists_push {α : Type u_1} {n : Nat} {xs : Vector α (n + 1)} : ∃ (ys : Vector α n), ∃ (a : α), xs = ys.push a

theorem Vector.singleton_inj {α✝ : Type u_1} {a b : α✝} : #v[a] = #v[b] ↔ a = b

cast

@[simp]

theorem Vector.getElem_cast {α : Type u_1} {n m : Nat} {xs : Vector α n} {h : n = m} {i : Nat} (hi : i < m) : (Vector.cast h xs)[i] = xs[i]

@[simp]

theorem Vector.getElem?_cast {α : Type u_1} {n m : Nat} {xs : Vector α n} {w : n = m} {i : Nat} : (Vector.cast w xs)[i]? = xs[i]?

@[simp]

theorem Vector.mem_cast {α : Type u_1} {n m : Nat} {a : α} {xs : Vector α n} {w : n = m} : a ∈ Vector.cast w xs ↔ a ∈ xs

@[simp]

theorem Vector.cast_cast {α : Type u_1} {n m k : Nat} {xs : Vector α n} {w : n = m} {w' : m = k} : Vector.cast w' (Vector.cast w xs) = Vector.cast ⋯ xs

@[simp]

theorem Vector.cast_rfl {α : Type u_1} {n : Nat} {xs : Vector α n} : Vector.cast ⋯ xs = xs

@[simp]

theorem Vector.cast_eq_cast {α : Type u_1} {n m k : Nat} {as : Vector α n} {bs : Vector α m} {wa : n = k} {wb : m = k} : Vector.cast wa as = Vector.cast wb bs ↔ as = Vector.cast ⋯ bs

In an equality between two casts, push the casts to the right hand side.

replicate

@[simp]

theorem Vector.replicate_zero {α✝ : Type u_1} {a : α✝} : replicate 0 a = #v[]

theorem Vector.replicate_succ {n : Nat} {α✝ : Type u_1} {a : α✝} : replicate (n + 1) a = (replicate n a).push a

@[simp]

theorem Vector.replicate_inj {n : Nat} {α✝ : Type u_1} {a b : α✝} : replicate n a = replicate n b ↔ n = 0 ∨ a = b

@[simp]

theorem Array.vector_mk_replicate {α : Type u_1} {a : α} {n : Nat} : Vector.mk (replicate n a) ⋯ = Vector.replicate n a

theorem Vector.replicate_eq_mk_replicate {α : Type u_1} {a : α} {n : Nat} : replicate n a = mk (Array.replicate n a) ⋯

L[i] and L[i]?

theorem Vector.getElem?_eq_none_iff {α : Type u_1} {n i : Nat} {xs : Vector α n} : xs[i]? = none ↔ n ≤ i

theorem Vector.none_eq_getElem?_iff {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : none = xs[i]? ↔ n ≤ i

theorem Vector.getElem?_eq_none {α : Type u_1} {n i : Nat} {xs : Vector α n} (h : n ≤ i) : xs[i]? = none

@[simp]

theorem Vector.getElem?_eq_getElem {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i]

theorem Vector.getElem?_eq_some_iff {α : Type u_1} {n i : Nat} {b : α} {xs : Vector α n} : xs[i]? = some b ↔ ∃ (h : i < n), xs[i] = b

theorem Vector.getElem_of_getElem? {α : Type u_1} {n i : Nat} {a : α} {xs : Vector α n} : xs[i]? = some a → ∃ (h : i < n), xs[i] = a

theorem Vector.some_eq_getElem?_iff {α : Type u_1} {n : Nat} {b : α} {i : Nat} {xs : Vector α n} : some b = xs[i]? ↔ ∃ (h : i < n), xs[i] = b

theorem Vector.some_getElem_eq_getElem?_iff {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : some xs[i] = xs[i]? ↔ True

theorem Vector.getElem?_eq_some_getElem_iff {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i] ↔ True

theorem Vector.getElem_eq_iff {α : Type u_1} {n : Nat} {x : α} {xs : Vector α n} {i : Nat} {h : i < n} : xs[i] = x ↔ xs[i]? = some x

theorem Vector.getElem_eq_getElem?_get {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs[i] = xs[i]?.get ⋯

theorem Vector.getD_getElem? {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {d : α} : xs[i]?.getD d = if p : i < n then xs[i] else d

@[simp]

theorem Vector.getElem?_empty {α : Type u_1} {i : Nat} : #v[][i]? = none

@[simp]

theorem Vector.getElem_push_lt {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} {i : Nat} (h : i < n) : (xs.push x)[i] = xs[i]

@[simp]

theorem Vector.getElem_push_eq {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} : (xs.push x)[n] = x

theorem Vector.getElem_push {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} {i : Nat} (h : i < n + 1) : (xs.push x)[i] = if h : i < n then xs[i] else x

theorem Vector.getElem?_push {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} {i : Nat} : (xs.push x)[i]? = if i = n then some x else xs[i]?

theorem Vector.getElem?_push_size {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} : (xs.push x)[n]? = some x

theorem Vector.getElem_singleton {α : Type u_1} {i : Nat} {a : α} (h : i < 1) : #v[a][i] = a

theorem Vector.getElem?_singleton {α : Type u_1} {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a else none

mem

@[simp]

theorem Vector.getElem_mem {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs[i] ∈ xs

theorem Vector.not_mem_empty {α : Type u_1} (a : α) : ¬a ∈ #v[]

@[simp]

theorem Vector.mem_push {α : Type u_1} {n : Nat} {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y

theorem Vector.mem_or_eq_of_mem_push {α : Type u_1} {n : Nat} {a b : α} {xs : Vector α n} : a ∈ xs.push b → a ∈ xs ∨ a = b

theorem Vector.mem_push_self {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} : x ∈ xs.push x

theorem Vector.eq_push_append_of_mem {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} (h : x ∈ xs) : ∃ (n₁ : Nat), ∃ (n₂ : Nat), ∃ (as : Vector α n₁), ∃ (bs : Vector α n₂), ∃ (h : n₁ + 1 + n₂ = n), xs = Vector.cast h (as.push x ++ bs) ∧ ¬x ∈ as

theorem Vector.mem_push_of_mem {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} (y : α) (h : x ∈ xs) : x ∈ xs.push y

theorem Vector.exists_mem_of_size_pos {α : Type u_1} {n : Nat} {xs : Vector α n} (h : 0 < n) : ∃ (x : α), x ∈ xs

theorem Vector.size_zero_iff_forall_not_mem {α : Type u_1} {n : Nat} {xs : Vector α n} : n = 0 ↔ ∀ (a : α), ¬a ∈ xs

@[simp]

theorem Vector.mem_dite_empty_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : ¬p → Vector α 0} : (x ∈ if h : p then #v[] else xs h) ↔ ∃ (h : ¬p), x ∈ xs h

@[simp]

theorem Vector.mem_dite_empty_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : p → Vector α 0} : (x ∈ if h : p then xs h else #v[]) ↔ ∃ (h : p), x ∈ xs h

@[simp]

theorem Vector.mem_ite_empty_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : Vector α 0} : (x ∈ if p then #v[] else xs) ↔ ¬p ∧ x ∈ xs

@[simp]

theorem Vector.mem_ite_empty_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : Vector α 0} : (x ∈ if p then xs else #v[]) ↔ p ∧ x ∈ xs

theorem Vector.eq_of_mem_singleton {α✝ : Type u_1} {b a : α✝} (h : a ∈ #v[b]) : a = b

theorem Vector.mem_singleton {α : Type u_1} {a b : α} : a ∈ #v[b] ↔ a = b

theorem Vector.forall_mem_push {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector α n} {a : α} : (∀ (x : α), x ∈ xs.push a → p x) ↔ p a ∧ ∀ (x : α), x ∈ xs → p x

theorem Vector.forall_mem_ne {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : (∀ (a' : α), a' ∈ xs → ¬a = a') ↔ ¬a ∈ xs

theorem Vector.forall_mem_ne' {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : (∀ (a' : α), a' ∈ xs → ¬a' = a) ↔ ¬a ∈ xs

theorem Vector.exists_mem_empty {α : Type u_1} (p : α → Prop) : ¬∃ (x : α), ∃ (x_1 : x ∈ #v[]), p x

theorem Vector.forall_mem_empty {α : Type u_1} (p : α → Prop) (x : α) : x ∈ #v[] → p x

theorem Vector.exists_mem_push {α : Type u_1} {n : Nat} {p : α → Prop} {a : α} {xs : Vector α n} : (∃ (x : α), ∃ (x_1 : x ∈ xs.push a), p x) ↔ p a ∨ ∃ (x : α), ∃ (x_1 : x ∈ xs), p x

theorem Vector.forall_mem_singleton {α : Type u_1} {p : α → Prop} {a : α} : (∀ (x : α), x ∈ #v[a] → p x) ↔ p a

theorem Vector.mem_empty_iff {α : Type u_1} (a : α) : a ∈ #v[] ↔ False

theorem Vector.mem_singleton_self {α : Type u_1} (a : α) : a ∈ #v[a]

theorem Vector.mem_of_mem_push_of_mem {α : Type u_1} {n : Nat} {a b : α} {xs : Vector α n} : a ∈ xs.push b → b ∈ xs → a ∈ xs

theorem Vector.eq_or_ne_mem_of_mem {α : Type u_1} {n : Nat} {a b : α} {xs : Vector α n} (h' : a ∈ xs.push b) : a = b ∨ a ≠ b ∧ a ∈ xs

theorem Vector.size_ne_zero_of_mem {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} (h : a ∈ xs) : n ≠ 0

theorem Vector.mem_of_ne_of_mem {α : Type u_1} {n : Nat} {a y : α} {xs : Vector α n} (h₁ : a ≠ y) (h₂ : a ∈ xs.push y) : a ∈ xs

theorem Vector.ne_of_not_mem_push {α : Type u_1} {n : Nat} {a b : α} {xs : Vector α n} (h : ¬a ∈ xs.push b) : a ≠ b

theorem Vector.not_mem_of_not_mem_push {α : Type u_1} {n : Nat} {a b : α} {xs : Vector α n} (h : ¬a ∈ xs.push b) : ¬a ∈ xs

theorem Vector.not_mem_push_of_ne_of_not_mem {α : Type u_1} {n : Nat} {a y : α} {xs : Vector α n} : a ≠ y → ¬a ∈ xs → ¬a ∈ xs.push y

theorem Vector.ne_and_not_mem_of_not_mem_push {α : Type u_1} {n : Nat} {a y : α} {xs : Vector α n} : ¬a ∈ xs.push y → a ≠ y ∧ ¬a ∈ xs

theorem Vector.getElem_of_mem {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} (h : a ∈ xs) : ∃ (i : Nat), ∃ (h : i < n), xs[i] = a

theorem Vector.getElem?_of_mem {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} (h : a ∈ xs) : ∃ (i : Nat), xs[i]? = some a

theorem Vector.mem_of_getElem {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {h : i < n} {a : α} (e : xs[i] = a) : a ∈ xs

theorem Vector.mem_of_getElem? {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {a : α} (e : xs[i]? = some a) : a ∈ xs

theorem Vector.mem_of_back? {α : Type u_1} {n : Nat} {xs : Vector α n} {a : α} (h : xs.back? = some a) : a ∈ xs

theorem Vector.mem_iff_getElem {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : a ∈ xs ↔ ∃ (i : Nat), ∃ (h : i < n), xs[i] = a

theorem Vector.mem_iff_getElem? {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : a ∈ xs ↔ ∃ (i : Nat), xs[i]? = some a

theorem Vector.exists_mem_iff_exists_getElem {α : Type u_1} {n : Nat} {P : α → Prop} {xs : Vector α n} : (∃ (x : α), x ∈ xs ∧ P x) ↔ ∃ (i : Nat), ∃ (hi : i < n), P xs[i]

theorem Vector.forall_mem_iff_forall_getElem {α : Type u_1} {n : Nat} {P : α → Prop} {xs : Vector α n} : (∀ (x : α), x ∈ xs → P x) ↔ ∀ (i : Nat) (hi : i < n), P xs[i]

@[deprecated Vector.forall_mem_iff_forall_getElem (since := "2026-01-29")]

theorem Vector.forall_getElem {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Prop} : (∀ (i : Nat) (h : i < n), p xs[i]) ↔ ∀ (a : α), a ∈ xs → p a

Decidability of bounded quantifiers

@[implicit_reducible]

instance Vector.instDecidableForallForallMemOfDecidablePred {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Prop} [DecidablePred p] : Decidable (∀ (x : α), x ∈ xs → p x)

Equations

• Vector.instDecidableForallForallMemOfDecidablePred = decidable_of_iff (∀ (i : Nat) (h : i < n), p xs[i]) ⋯

@[implicit_reducible]

instance Vector.instDecidableExistsAndMemOfDecidablePred {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Prop} [DecidablePred p] : Decidable (∃ (x : α), x ∈ xs ∧ p x)

Equations

• Vector.instDecidableExistsAndMemOfDecidablePred = decidable_of_iff (∃ (i : Nat), ∃ (h : i < n), p xs[i]) ⋯

any / all

theorem Vector.any_iff_exists {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.any p = true ↔ ∃ (i : Nat), ∃ (x : i < n), p xs[i] = true

theorem Vector.all_iff_forall {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.all p = true ↔ ∀ (i : Nat) (x : i < n), p xs[i] = true

theorem Vector.any_eq_true {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.any p = true ↔ ∃ (i : Nat), ∃ (x : i < n), p xs[i] = true

theorem Vector.any_eq_false {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.any p = false ↔ ∀ (i : Nat) (x : i < n), ¬p xs[i] = true

theorem Vector.allM_eq_not_anyM_not {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n} : allM p xs = (fun (x : Bool) => !x) <$> anyM (fun (x : α) => (fun (x : Bool) => !x) <$> p x) xs

theorem Vector.all_eq_not_any_not {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.all p = !xs.any fun (x : α) => !p x

@[simp]

theorem Vector.all_eq_true {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.all p = true ↔ ∀ (i : Nat) (x : i < n), p xs[i] = true

@[simp]

theorem Vector.all_eq_false {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.all p = false ↔ ∃ (i : Nat), ∃ (x : i < n), ¬p xs[i] = true

theorem Vector.all_eq_true_iff_forall_mem {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true

theorem Vector.any_eq_true' {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.any p = true ↔ ∃ (x : α), x ∈ xs ∧ p x = true

Variant of any_eq_true in terms of membership rather than an array index.

theorem Vector.any_eq_false' {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.any p = false ↔ ∀ (x : α), x ∈ xs → ¬p x = true

Variant of any_eq_false in terms of membership rather than an array index.

theorem Vector.all_eq_true' {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true

Variant of all_eq_true in terms of membership rather than an array index.

theorem Vector.all_eq_false' {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n} : xs.all p = false ↔ ∃ (x : α), x ∈ xs ∧ ¬p x = true

Variant of all_eq_false in terms of membership rather than an array index.

theorem Vector.any_eq {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ (i : Nat), ∃ (h : i < n), p xs[i] = true)

theorem Vector.any_eq' {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ (x : α), x ∈ xs ∧ p x = true)

Variant of any_eq in terms of membership rather than an array index.

theorem Vector.all_eq {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

theorem Vector.all_eq' {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Variant of all_eq in terms of membership rather than an array index.

theorem Vector.decide_exists_mem {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Prop} [DecidablePred p] : decide (∃ (x : α), x ∈ xs ∧ p x) = xs.any fun (b : α) => decide (p b)

theorem Vector.decide_forall_mem {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Prop} [DecidablePred p] : decide (∀ (x : α), x ∈ xs → p x) = xs.all fun (b : α) => decide (p b)

theorem Vector.any_beq {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {a : α} : (xs.any fun (x : α) => a == x) = xs.contains a

theorem Vector.any_beq' {α : Type u_1} {n : Nat} {a : α} [BEq α] [PartialEquivBEq α] {xs : Vector α n} : (xs.any fun (x : α) => x == a) = xs.contains a

Variant of any_beq with == reversed.

theorem Vector.all_bne {α : Type u_1} {n : Nat} {a : α} [BEq α] {xs : Vector α n} : (xs.all fun (x : α) => a != x) = !xs.contains a

theorem Vector.all_bne' {α : Type u_1} {n : Nat} {a : α} [BEq α] [PartialEquivBEq α] {xs : Vector α n} : (xs.all fun (x : α) => x != a) = !xs.contains a

Variant of all_bne with != reversed.

theorem Vector.mem_of_contains_eq_true {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} : as.contains a = true → a ∈ as

theorem Vector.contains_eq_true_of_mem {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} (h : a ∈ as) : as.contains a = true

theorem Vector.contains_iff_mem {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} : as.contains a = true ↔ a ∈ as

@[deprecated Vector.contains_iff_mem (since := "2025-10-26")]

theorem Vector.contains_iff {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} : as.contains a = true ↔ a ∈ as

@[implicit_reducible]

instance Vector.instDecidableMemOfLawfulBEq {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈ as)

Equations

• Vector.instDecidableMemOfLawfulBEq a as = decidable_of_decidable_of_iff ⋯

theorem Vector.contains_empty {α : Type u_1} {a : α} [BEq α] : #v[].contains a = false

@[simp]

theorem Vector.contains_eq_mem {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} : as.contains a = decide (a ∈ as)

@[simp]

theorem Vector.any_push {α : Type u_1} {n : Nat} {as : Vector α n} {a : α} {p : α → Bool} : (as.push a).any p = (as.any p || p a)

@[simp]

theorem Vector.all_push {α : Type u_1} {n : Nat} {as : Vector α n} {a : α} {p : α → Bool} : (as.push a).all p = (as.all p && p a)

@[simp]

theorem Vector.contains_push {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {a b : α} : (xs.push a).contains b = (xs.contains b || b == a)

set

theorem Vector.getElem_set {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} (hi : i < n) {j : Nat} (hj : j < n) : (xs.set i x hi)[j] = if i = j then x else xs[j]

@[simp]

theorem Vector.getElem_set_self {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} (hi : i < n) : (xs.set i x hi)[i] = x

@[simp]

theorem Vector.getElem_set_ne {α : Type u_1} {n i j : Nat} {xs : Vector α n} {x : α} (hi : i < n) (hj : j < n) (h : i ≠ j) : (xs.set i x hi)[j] = xs[j]

theorem Vector.getElem?_set {α : Type u_1} {n i j : Nat} {xs : Vector α n} {x : α} (hi : i < n) : (xs.set i x hi)[j]? = if i = j then some x else xs[j]?

@[simp]

theorem Vector.getElem?_set_self {α : Type u_1} {n i : Nat} {xs : Vector α n} {x : α} (hi : i < n) : (xs.set i x hi)[i]? = some x

@[simp]

theorem Vector.getElem?_set_ne {α : Type u_1} {n i j : Nat} {xs : Vector α n} {x : α} (hi : i < n) (h : i ≠ j) : (xs.set i x hi)[j]? = xs[j]?

@[simp]

theorem Vector.set_getElem_self {α : Type u_1} {n i : Nat} {xs : Vector α n} (hi : i < n) : xs.set i xs[i] hi = xs

theorem Vector.set_push {α : Type u_1} {n i : Nat} {xs : Vector α n} {x y : α} {h : i < n + 1} : (xs.push x).set i y h = if x_1 : i < n then (xs.set i y x_1).push x else xs.push y

theorem Vector.set_comm {α : Type u_1} {n i j : Nat} (a b : α) {xs : Vector α n} {hi : i < n} {hj : j < n} (h : i ≠ j) : (xs.set i a hi).set j b hj = (xs.set j b hj).set i a hi

@[simp]

theorem Vector.set_set {α : Type u_1} {n i : Nat} (a : α) {b : α} {xs : Vector α n} (hi : i < n) : (xs.set i a hi).set i b hi = xs.set i b hi

theorem Vector.mem_set {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {a : α} (hi : i < n) : a ∈ xs.set i a hi

theorem Vector.mem_or_eq_of_mem_set {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {a b : α} {hi : i < n} (h : a ∈ xs.set i b hi) : a ∈ xs ∨ a = b

setIfInBounds

@[simp]

theorem Vector.setIfInBounds_empty {α : Type u_1} {i : Nat} {a : α} : #v[].setIfInBounds i a = #v[]

theorem Vector.getElem_setIfInBounds {α : Type u_1} {n j i : Nat} {xs : Vector α n} {x : α} (hj : j < n) : (xs.setIfInBounds i x)[j] = if i = j then x else xs[j]

@[simp]

theorem Vector.getElem_setIfInBounds_self {α : Type u_1} {n i : Nat} {xs : Vector α n} {x : α} (hi : i < n) : (xs.setIfInBounds i x)[i] = x

@[simp]

theorem Vector.getElem_setIfInBounds_ne {α : Type u_1} {n j i : Nat} {xs : Vector α n} {x : α} (hj : j < n) (h : i ≠ j) : (xs.setIfInBounds i x)[j] = xs[j]

theorem Vector.getElem?_setIfInBounds {α : Type u_1} {n i j : Nat} {xs : Vector α n} {x : α} : (xs.setIfInBounds i x)[j]? = if i = j then if i < n then some x else none else xs[j]?

theorem Vector.getElem?_setIfInBounds_self {α : Type u_1} {n i : Nat} {xs : Vector α n} {x : α} : (xs.setIfInBounds i x)[i]? = if i < n then some x else none

@[simp]

theorem Vector.getElem?_setIfInBounds_self_of_lt {α : Type u_1} {n i : Nat} {xs : Vector α n} {x : α} (h : i < n) : (xs.setIfInBounds i x)[i]? = some x

@[simp]

theorem Vector.getElem?_setIfInBounds_ne {α : Type u_1} {n i j : Nat} {xs : Vector α n} {x : α} (h : i ≠ j) : (xs.setIfInBounds i x)[j]? = xs[j]?

theorem Vector.setIfInBounds_eq_of_size_le {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : n ≤ i) {a : α} : xs.setIfInBounds i a = xs

theorem Vector.setIfInBound_comm {α : Type u_1} {n : Nat} (a b : α) {i j : Nat} {xs : Vector α n} (h : i ≠ j) : (xs.setIfInBounds i a).setIfInBounds j b = (xs.setIfInBounds j b).setIfInBounds i a

@[simp]

theorem Vector.setIfInBounds_setIfInBounds {α : Type u_1} {n i : Nat} (a : α) {b : α} {xs : Vector α n} : (xs.setIfInBounds i a).setIfInBounds i b = xs.setIfInBounds i b

theorem Vector.mem_setIfInBounds {α : Type u_1} {n i : Nat} {xs : Vector α n} {a : α} (hi : i < n) : a ∈ xs.setIfInBounds i a

BEq

@[simp]

theorem Vector.push_beq_push {α : Type u_1} [BEq α] {a b : α} {n : Nat} {xs ys : Vector α n} : (xs.push a == ys.push b) = (xs == ys && a == b)

@[simp, irreducible]

theorem Vector.replicate_beq_replicate {α : Type u_1} [BEq α] {a b : α} {n : Nat} : (replicate n a == replicate n b) = (n == 0 || a == b)

@[simp]

theorem Vector.reflBEq_iff {α : Type u_1} {n : Nat} [BEq α] [NeZero n] : ReflBEq (Vector α n) ↔ ReflBEq α

@[simp]

theorem Vector.lawfulBEq_iff {α : Type u_1} {n : Nat} [BEq α] [NeZero n] : LawfulBEq (Vector α n) ↔ LawfulBEq α

isEqv

@[simp]

theorem Vector.isEqv_eq {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {xs ys : Vector α n} : ((xs.isEqv ys fun (x1 x2 : α) => x1 == x2) = true) = (xs = ys)

back

theorem Vector.back_singleton {α : Type u_1} {a : α} : #v[a].back = a

theorem Vector.back_eq_getElem {n : Nat} {α : Type u_1} [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]

theorem Vector.back?_empty {α : Type u_1} : #v[].back? = none

theorem Vector.back?_eq_getElem? {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.back? = xs[n - 1]?

@[simp]

theorem Vector.back_mem {n : Nat} {α : Type u_1} [NeZero n] {xs : Vector α n} : xs.back ∈ xs

map

@[simp]

theorem Vector.getElem_map {α : Type u_1} {β : Type u_2} {n i : Nat} (f : α → β) {xs : Vector α n} (hi : i < n) : (map f xs)[i] = f xs[i]

@[simp]

theorem Vector.getElem?_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} {i : Nat} : (map f xs)[i]? = Option.map f xs[i]?

theorem Vector.map_empty {α : Type u_1} {β : Type u_2} {f : α → β} : map f #v[] = #v[]

The empty vector maps to the empty vector.

@[simp]

theorem Vector.map_push {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {as : Vector α n} {x : α} : map f (as.push x) = (map f as).push (f x)

@[simp]

theorem Vector.map_id_fun {n : Nat} {α : Type u_1} : map id = id

@[simp]

theorem Vector.map_id_fun' {n : Nat} {α : Type u_1} : (map fun (a : α) => a) = id

map_id_fun' differs from map_id_fun by representing the identity function as a lambda, rather than id.

theorem Vector.map_id {α : Type u_1} {n : Nat} (xs : Vector α n) : map id xs = xs

theorem Vector.map_id' {α : Type u_1} {n : Nat} (xs : Vector α n) : map (fun (a : α) => a) xs = xs

map_id' differs from map_id by representing the identity function as a lambda, rather than id.

theorem Vector.map_id'' {α : Type u_1} {n : Nat} {f : α → α} (h : ∀ (x : α), f x = x) (xs : Vector α n) : map f xs = xs

Variant of map_id, with a side condition that the function is pointwise the identity.

theorem Vector.map_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : map f #v[a] = #v[f a]

@[simp]

theorem Vector.mem_map {α : Type u_1} {β : Type u_2} {n : Nat} {b : β} {f : α → β} {xs : Vector α n} : b ∈ map f xs ↔ ∃ (a : α), a ∈ xs ∧ f a = b

theorem Vector.exists_of_mem_map {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {n✝ : Nat} {xs : Vector α✝ n✝} {b : α✝¹} (h : b ∈ map f xs) : ∃ (a : α✝), a ∈ xs ∧ f a = b

theorem Vector.mem_map_of_mem {α : Type u_1} {β : Type u_2} {n✝ : Nat} {xs : Vector α n✝} {a : α} {f : α → β} (h : a ∈ xs) : f a ∈ map f xs

theorem Vector.forall_mem_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} {P : β → Prop} : (∀ (i : β), i ∈ map f xs → P i) ↔ ∀ (j : α), j ∈ xs → P (f j)

@[simp]

theorem Vector.map_inj_left {α : Type u_1} {β : Type u_2} {n✝ : Nat} {xs : Vector α n✝} {f g : α → β} : map f xs = map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a

theorem Vector.map_inj_right {α : Type u_1} {β : Type u_2} {n✝ : Nat} {xs ys : Vector α n✝} {f : α → β} (w : ∀ (x y : α), f x = f y → x = y) : map f xs = map f ys ↔ xs = ys

theorem Vector.map_congr_left {α✝ : Type u_1} {n✝ : Nat} {xs : Vector α✝ n✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} (h : ∀ (a : α✝), a ∈ xs → f a = g a) : map f xs = map g xs

theorem Vector.map_inj {n : Nat} {α✝ : Type u_1} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} [NeZero n] : map f = map g ↔ f = g

theorem Vector.map_eq_push_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α (n + 1)} {ys : Vector β n} {b : β} : map f xs = ys.push b ↔ ∃ (xs' : Vector α n), ∃ (a : α), xs = xs'.push a ∧ map f xs' = ys ∧ f a = b

theorem Vector.map_eq_singleton_iff {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Vector α 1} {b : β} : map f xs = #v[b] ↔ ∃ (a : α), xs = #v[a] ∧ f a = b

theorem Vector.map_eq_map_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f g : α → β} {xs : Vector α n} : map f xs = map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a

theorem Vector.map_eq_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {as : Vector α n} {bs : Vector β n} : map f as = bs ↔ ∀ (i : Nat) (h : i < n), bs[i] = f as[i]

@[simp]

theorem Vector.map_set {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} {i : Nat} {h : i < n} {a : α} : map f (xs.set i a h) = (map f xs).set i (f a) h

@[simp]

theorem Vector.map_setIfInBounds {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} {i : Nat} {a : α} : map f (xs.setIfInBounds i a) = (map f xs).setIfInBounds i (f a)

@[simp]

theorem Vector.map_pop {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} : map f xs.pop = (map f xs).pop

@[simp]

theorem Vector.back?_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} : (map f xs).back? = Option.map f xs.back?

@[simp]

theorem Vector.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β} {g : β → γ} {as : Vector α n} : map g (map f as) = map (g ∘ f) as

theorem Vector.vector₂_induction {α : Type u_1} {n m : Nat} (P : Vector (Vector α n) m → Prop) (of : ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = n), P (mk (Array.map (fun (x : { x : Array α // x ∈ xss }) => match x with | ⟨xs, m⟩ => mk xs ⋯) xss.attach) ⋯)) (xss : Vector (Vector α n) m) : P xss

Use this as induction ass using vector₂_induction on a hypothesis of the form ass : Vector (Vector α n) m. The hypothesis ass will be replaced with a hypothesis ass : Array (Array α) along with additional hypotheses h₁ : ass.size = m and h₂ : ∀ xs ∈ ass, xs.size = n. Appearances of the original ass in the goal will be replaced with Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk xs ⋯)) ⋯.

theorem Vector.vector₃_induction {α : Type u_1} {n m k : Nat} (P : Vector (Vector (Vector α n) m) k → Prop) (of : ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m) (h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (as : Array α), as ∈ xs → as.size = n), P (mk (Array.map (fun (x : { x : Array (Array α) // x ∈ xss }) => match x with | ⟨xs, m_1⟩ => mk (Array.map (fun (x : { x : Array α // x ∈ xs }) => match x with | ⟨as, m'⟩ => mk as ⋯) xs.attach) ⋯) xss.attach) ⋯)) (xss : Vector (Vector (Vector α n) m) k) : P xss

Use this as induction ass using vector₃_induction on a hypothesis of the form ass : Vector (Vector (Vector α n) m) k. The hypothesis ass will be replaced with a hypothesis ass : Array (Array (Array α)) along with additional hypotheses h₁ : ass.size = k, h₂ : ∀ xs ∈ ass, xs.size = m, and h₃ : ∀ xs ∈ ass, ∀ x ∈ xs, x.size = n. Appearances of the original ass in the goal will be replaced with Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk (xs.attach.map (fun ⟨x, m'⟩ => Vector.mk x ⋯)) ⋯)) ⋯.

singleton

@[simp]

theorem Vector.singleton_def {α : Type u_1} {v : α} : singleton v = #v[v]

append

@[simp]

theorem Vector.push_append {α : Type u_1} {n m : Nat} {as : Vector α n} {bs : Vector α m} {a : α} : (as ++ bs).push a = as ++ bs.push a

theorem Vector.append_push {α : Type u_1} {n m : Nat} {as : Vector α n} {bs : Vector α m} {a : α} : as ++ bs.push a = (as ++ bs).push a

theorem Vector.singleton_eq_toVector_singleton {α : Type u_1} {a : α} : #v[a] = #[a].toVector

@[simp]

theorem Vector.mem_append {α : Type u_1} {n m : Nat} {a : α} {xs : Vector α n} {ys : Vector α m} : a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys

theorem Vector.mem_append_left {α : Type u_1} {n m : Nat} {a : α} {xs : Vector α n} (ys : Vector α m) (h : a ∈ xs) : a ∈ xs ++ ys

theorem Vector.mem_append_right {α : Type u_1} {n m : Nat} {a : α} (xs : Vector α n) {ys : Vector α m} (h : a ∈ ys) : a ∈ xs ++ ys

theorem Vector.not_mem_append {α : Type u_1} {n m : Nat} {a : α} {xs : Vector α n} {ys : Vector α m} (h₁ : ¬a ∈ xs) (h₂ : ¬a ∈ ys) : ¬a ∈ xs ++ ys

theorem Vector.append_of_mem {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} (h : a ∈ xs) : ∃ (m : Nat), ∃ (k : Nat), ∃ (w : m + 1 + k = n), ∃ (ys : Vector α m), ∃ (zs : Vector α k), xs = Vector.cast w (ys.push a ++ zs)

See also eq_push_append_of_mem, which proves a stronger version in which the initial array must not contain the element.

theorem Vector.mem_iff_append {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : a ∈ xs ↔ ∃ (m : Nat), ∃ (k : Nat), ∃ (w : m + 1 + k = n), ∃ (ys : Vector α m), ∃ (zs : Vector α k), xs = Vector.cast w (ys.push a ++ zs)

theorem Vector.forall_mem_append {α : Type u_1} {n m : Nat} {p : α → Prop} {xs : Vector α n} {ys : Vector α m} : (∀ (x : α), x ∈ xs ++ ys → p x) ↔ (∀ (x : α), x ∈ xs → p x) ∧ ∀ (x : α), x ∈ ys → p x

@[simp]

theorem Vector.empty_append {α : Type u_1} {n : Nat} {xs : Vector α n} : #v[] ++ xs = Vector.cast ⋯ xs

@[simp]

theorem Vector.append_empty {α : Type u_1} {n : Nat} {xs : Vector α n} : xs ++ #v[] = xs

theorem Vector.getElem_append {α : Type u_1} {n m i : Nat} {xs : Vector α n} {ys : Vector α m} (hi : i < n + m) : (xs ++ ys)[i] = if h : i < n then xs[i] else ys[i - n]

@[simp]

theorem Vector.getElem_append_left {α : Type u_1} {n m i : Nat} {xs : Vector α n} {ys : Vector α m} (hi : i < n) : (xs ++ ys)[i] = xs[i]

@[simp]

theorem Vector.getElem_append_right {α : Type u_1} {n m i : Nat} {xs : Vector α n} {ys : Vector α m} (h : i < n + m) (hi : n ≤ i) : (xs ++ ys)[i] = ys[i - n]

theorem Vector.getElem?_append_left {α : Type u_1} {n m i : Nat} {xs : Vector α n} {ys : Vector α m} (hn : i < n) : (xs ++ ys)[i]? = xs[i]?

theorem Vector.getElem?_append_right {α : Type u_1} {n m i : Nat} {xs : Vector α n} {ys : Vector α m} (h : n ≤ i) : (xs ++ ys)[i]? = ys[i - n]?

theorem Vector.getElem?_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i : Nat} : (xs ++ ys)[i]? = if i < n then xs[i]? else ys[i - n]?

theorem Vector.getElem_append_left' {α : Type u_1} {m i n : Nat} {xs : Vector α m} (hi : i < m) (ys : Vector α n) : xs[i] = (xs ++ ys)[i]

Variant of getElem_append_left useful for rewriting from the small array to the big array.

theorem Vector.getElem_append_right' {α : Type u_1} {m n i : Nat} (xs : Vector α m) {ys : Vector α n} (hi : i < n) : ys[i] = (xs ++ ys)[i + m]

Variant of getElem_append_right useful for rewriting from the small array to the big array.

theorem Vector.getElem_of_append {α : Type u_1} {n m k : Nat} {a : α} {xs : Vector α n} {xs₁ : Vector α m} {xs₂ : Vector α k} (w : m + 1 + k = n) (eq : xs = Vector.cast w (xs₁.push a ++ xs₂)) : xs[m] = a

@[simp]

theorem Vector.append_singleton {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : xs ++ #v[a] = xs.push a

theorem Vector.append_inj {α : Type u_1} {n m : Nat} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) : xs₁ = xs₂ ∧ ys₁ = ys₂

theorem Vector.append_inj_right {α : Type u_1} {n m : Nat} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) : ys₁ = ys₂

theorem Vector.append_inj_left {α : Type u_1} {n m : Nat} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) : xs₁ = xs₂

theorem Vector.append_right_inj {α : Type u_1} {m n : Nat} {ys₁ ys₂ : Vector α m} (xs : Vector α n) : xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂

theorem Vector.append_left_inj {α : Type u_1} {n m : Nat} {xs₁ xs₂ : Vector α n} (ys : Vector α m) : xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂

theorem Vector.append_eq_append_iff {α : Type u_1} {n m k l : Nat} {ws : Vector α n} {xs : Vector α m} {ys : Vector α k} {zs : Vector α l} (w : k + l = n + m) : ws ++ xs = Vector.cast w (ys ++ zs) ↔ if h : n ≤ k then ∃ (as : Vector α (k - n)), ys = Vector.cast ⋯ (ws ++ as) ∧ xs = Vector.cast ⋯ (as ++ zs) else ∃ (cs : Vector α (n - k)), ws = Vector.cast ⋯ (ys ++ cs) ∧ zs = Vector.cast ⋯ (cs ++ xs)

@[simp]

theorem Vector.append_assoc {α : Type u_1} {n m k : Nat} {xs : Vector α n} {ys : Vector α m} {zs : Vector α k} : xs ++ ys ++ zs = Vector.cast ⋯ (xs ++ (ys ++ zs))

theorem Vector.append_assoc_symm {α : Type u_1} {n m k : Nat} {xs : Vector α n} {ys : Vector α m} {zs : Vector α k} : xs ++ (ys ++ zs) = Vector.cast ⋯ (xs ++ ys ++ zs)

theorem Vector.set_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h : i < n + m) : (xs ++ ys).set i x h = if h' : i < n then xs.set i x h' ++ ys else xs ++ ys.set (i - n) x ⋯

@[simp]

theorem Vector.set_append_left {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h : i < n) : (xs ++ ys).set i x ⋯ = xs.set i x h ++ ys

@[simp]

theorem Vector.set_append_right {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h' : i < n + m) (h : n ≤ i) : (xs ++ ys).set i x h' = xs ++ ys.set (i - n) x ⋯

theorem Vector.setIfInBounds_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} : (xs ++ ys).setIfInBounds i x = if i < n then xs.setIfInBounds i x ++ ys else xs ++ ys.setIfInBounds (i - n) x

@[simp]

theorem Vector.setIfInBounds_append_left {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h : i < n) : (xs ++ ys).setIfInBounds i x = xs.setIfInBounds i x ++ ys

@[simp]

theorem Vector.setIfInBounds_append_right {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h : n ≤ i) : (xs ++ ys).setIfInBounds i x = xs ++ ys.setIfInBounds (i - n) x

@[simp]

theorem Vector.map_append {α : Type u_1} {β : Type u_2} {n m : Nat} {f : α → β} {xs : Vector α n} {ys : Vector α m} : map f (xs ++ ys) = map f xs ++ map f ys

theorem Vector.map_eq_append_iff {α : Type u_1} {β : Type u_2} {a✝ a✝¹ : Nat} {xs : Vector α (a✝ + a✝¹)} {ys : Vector β a✝} {zs : Vector β a✝¹} {f : α → β} : map f xs = ys ++ zs ↔ ∃ (as : Vector α a✝), ∃ (bs : Vector α a✝¹), xs = as ++ bs ∧ map f as = ys ∧ map f bs = zs

theorem Vector.append_eq_map_iff {α : Type u_1} {β : Type u_2} {n✝ : Nat} {xs : Vector β n✝} {n✝¹ : Nat} {ys : Vector β n✝¹} {zs : Vector α (n✝ + n✝¹)} {f : α → β} : xs ++ ys = map f zs ↔ ∃ (as : Vector α n✝), ∃ (bs : Vector α n✝¹), zs = as ++ bs ∧ map f as = xs ∧ map f bs = ys

flatten

@[simp]

theorem Vector.flatten_mk {α : Type u_1} {n m : Nat} {xss : Array (Vector α n)} (h : xss.size = m) : (mk xss h).flatten = mk (Array.map toArray xss).flatten ⋯

@[simp]

theorem Vector.getElem_flatten {β : Type u_1} {m n : Nat} {xss : Vector (Vector β m) n} {i : Nat} (hi : i < n * m) : xss.flatten[i] = xss[i / m][i % m]

theorem Vector.getElem?_flatten {β : Type u_1} {m n : Nat} {xss : Vector (Vector β m) n} {i : Nat} : xss.flatten[i]? = if hi : i < n * m then some xss[i / m][i % m] else none

@[simp]

theorem Vector.flatten_singleton {α : Type u_1} {n : Nat} {xs : Vector α n} : #v[xs].flatten = Vector.cast ⋯ xs

theorem Vector.mem_flatten {α : Type u_1} {n m : Nat} {a : α} {xss : Vector (Vector α n) m} : a ∈ xss.flatten ↔ ∃ (xs : Vector α n), xs ∈ xss ∧ a ∈ xs

theorem Vector.exists_of_mem_flatten {α✝ : Type u_1} {n✝ n✝¹ : Nat} {xss : Vector (Vector α✝ n✝) n✝¹} {xs : α✝} : xs ∈ xss.flatten → ∃ (ys : Vector α✝ n✝), ys ∈ xss ∧ xs ∈ ys

theorem Vector.mem_flatten_of_mem {α✝ : Type u_1} {n✝ n✝¹ : Nat} {xss : Vector (Vector α✝ n✝) n✝¹} {xs : Vector α✝ n✝} {a : α✝} (ml : xs ∈ xss) (ma : a ∈ xs) : a ∈ xss.flatten

theorem Vector.forall_mem_flatten {α : Type u_1} {n m : Nat} {p : α → Prop} {xss : Vector (Vector α n) m} : (∀ (x : α), x ∈ xss.flatten → p x) ↔ ∀ (xs : Vector α n), xs ∈ xss → ∀ (x : α), x ∈ xs → p x

@[simp]

theorem Vector.map_flatten {α : Type u_1} {β : Type u_2} {n m : Nat} {f : α → β} {xss : Vector (Vector α n) m} : map f xss.flatten = (map (map f) xss).flatten

@[simp]

theorem Vector.flatten_append {α : Type u_1} {n m₁ m₂ : Nat} {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} : (xss₁ ++ xss₂).flatten = Vector.cast ⋯ (xss₁.flatten ++ xss₂.flatten)

theorem Vector.append_flatten {α : Type u_1} {n m₁ m₂ : Nat} {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} : xss₁.flatten ++ xss₂.flatten = Vector.cast ⋯ (xss₁ ++ xss₂).flatten

theorem Vector.flatten_push {α : Type u_1} {n m : Nat} {xss : Vector (Vector α n) m} {xs : Vector α n} : (xss.push xs).flatten = Vector.cast ⋯ (xss.flatten ++ xs)

theorem Vector.flatten_flatten {α : Type u_1} {n m k : Nat} {xss : Vector (Vector (Vector α n) m) k} : xss.flatten.flatten = Vector.cast ⋯ (map flatten xss).flatten

theorem Vector.eq_iff_flatten_eq {α : Type u_1} {n m : Nat} {xss xss' : Vector (Vector α n) m} : xss = xss' ↔ xss.flatten = xss'.flatten

Two vectors of constant length vectors are equal iff their flattens coincide.

flatMap

@[simp]

theorem Vector.flatMap_toArray {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} : Array.flatMap (fun (a : α) => (f a).toArray) xs.toArray = (xs.flatMap f).toArray

theorem Vector.flatMap_def {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} : xs.flatMap f = (map f xs).flatten

@[simp]

theorem Vector.flatMap_empty {α : Type u_1} {β : Type u_2} {m : Nat} {f : α → Vector β m} : #v[].flatMap f = Vector.cast ⋯ #v[]

@[simp]

theorem Vector.flatMap_push {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {x : α} {f : α → Vector β m} : (xs.push x).flatMap f = Vector.cast ⋯ (xs.flatMap f ++ f x)

@[simp]

theorem Vector.getElem_flatMap {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} {i : Nat} (hi : i < n * m) : (xs.flatMap f)[i] = (f xs[i / m])[i % m]

theorem Vector.getElem?_flatMap {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} {i : Nat} : (xs.flatMap f)[i]? = if hi : i < n * m then some (f xs[i / m])[i % m] else none

@[simp]

theorem Vector.flatMap_id {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} : xss.flatMap id = xss.flatten

@[simp]

theorem Vector.flatMap_id' {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} : (xss.flatMap fun (xs : Vector α m) => xs) = xss.flatten

@[simp]

theorem Vector.mem_flatMap {α : Type u_1} {β : Type u_2} {m n : Nat} {f : α → Vector β m} {b : β} {xs : Vector α n} : b ∈ xs.flatMap f ↔ ∃ (a : α), a ∈ xs ∧ b ∈ f a

theorem Vector.exists_of_mem_flatMap {β : Type u_1} {α : Type u_2} {n m : Nat} {b : β} {xs : Vector α n} {f : α → Vector β m} : b ∈ xs.flatMap f → ∃ (a : α), a ∈ xs ∧ b ∈ f a

theorem Vector.mem_flatMap_of_mem {β : Type u_1} {α : Type u_2} {n m : Nat} {b : β} {xs : Vector α n} {f : α → Vector β m} {a : α} (al : a ∈ xs) (h : b ∈ f a) : b ∈ xs.flatMap f

theorem Vector.forall_mem_flatMap {β : Type u_1} {α : Type u_2} {n m : Nat} {p : β → Prop} {xs : Vector α n} {f : α → Vector β m} : (∀ (x : β), x ∈ xs.flatMap f → p x) ↔ ∀ (a : α), a ∈ xs → ∀ (b : β), b ∈ f a → p b

theorem Vector.flatMap_singleton {α : Type u_1} {β : Type u_2} {m : Nat} {f : α → Vector β m} {x : α} : #v[x].flatMap f = Vector.cast ⋯ (f x)

@[simp]

theorem Vector.flatMap_singleton' {α : Type u_1} {n : Nat} {xs : Vector α n} : (xs.flatMap fun (x : α) => #v[x]) = Vector.cast ⋯ xs

@[simp]

theorem Vector.flatMap_append {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs ys : Vector α n} {f : α → Vector β m} : (xs ++ ys).flatMap f = Vector.cast ⋯ (xs.flatMap f ++ ys.flatMap f)

theorem Vector.flatMap_assoc {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {γ : Type u_3} {k : Nat} {xs : Vector α n} {f : α → Vector β m} {g : β → Vector γ k} : (xs.flatMap f).flatMap g = Vector.cast ⋯ (xs.flatMap fun (x : α) => (f x).flatMap g)

theorem Vector.map_flatMap {β : Type u_1} {γ : Type u_2} {α : Type u_3} {m n : Nat} {f : β → γ} {g : α → Vector β m} {xs : Vector α n} : map f (xs.flatMap g) = xs.flatMap fun (a : α) => map f (g a)

theorem Vector.flatMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {k n : Nat} {f : α → β} {g : β → Vector γ k} {xs : Vector α n} : (map f xs).flatMap g = xs.flatMap fun (a : α) => g (f a)

theorem Vector.map_eq_flatMap {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} : map f xs = Vector.cast ⋯ (xs.flatMap fun (x : α) => #v[f x])

replicate

@[simp]

theorem Vector.replicate_one {α✝ : Type u_1} {a : α✝} : replicate 1 a = #v[a]

theorem Vector.replicate_succ' {n : Nat} {α✝ : Type u_1} {a : α✝} : replicate (n + 1) a = Vector.cast ⋯ (#v[a] ++ replicate n a)

Variant of replicate_succ that prepends a at the beginning of the vector.

@[simp]

theorem Vector.mem_replicate {α : Type u_1} {a b : α} {n : Nat} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

theorem Vector.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : Nat} (h : b ∈ replicate n a) : b = a

theorem Vector.forall_mem_replicate {α : Type u_1} {p : α → Prop} {a : α} {n : Nat} : (∀ (b : α), b ∈ replicate n a → p b) ↔ n = 0 ∨ p a

@[simp]

theorem Vector.getElem_replicate {α : Type u_1} {i n : Nat} {a : α} (h : i < n) : (replicate n a)[i] = a

theorem Vector.getElem?_replicate {α : Type u_1} {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none

@[simp]

theorem Vector.getElem?_replicate_of_lt {α✝ : Type u_1} {a : α✝} {n i : Nat} (h : i < n) : (replicate n a)[i]? = some a

theorem Vector.eq_replicate_of_mem {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} (h : ∀ (b : α), b ∈ xs → b = a) : xs = replicate n a

theorem Vector.eq_replicate_iff {α : Type u_1} {a : α} {n : Nat} {xs : Vector α n} : xs = replicate n a ↔ ∀ (b : α), b ∈ xs → b = a

theorem Vector.map_eq_replicate_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : α → β} {b : β} : map f xs = replicate n b ↔ ∀ (x : α), x ∈ xs → f x = b

@[simp]

theorem Vector.map_const {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {b : β} : map (Function.const α b) xs = replicate n b

@[simp]

theorem Vector.map_const_fun {β : Type u_1} {n : Nat} {α : Type u_2} {x : β} : map (Function.const α x) = fun (x_1 : Vector α n) => replicate n x

theorem Vector.map_const' {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {b : β} : map (fun (x : α) => b) xs = replicate n b

Variant of map_const using a lambda rather than Function.const.

@[simp]

theorem Vector.set_replicate_self {n : Nat} {α✝ : Type u_1} {a : α✝} {i : Nat} {h : i < n} : (replicate n a).set i a h = replicate n a

@[simp]

theorem Vector.setIfInBounds_replicate_self {n : Nat} {α✝ : Type u_1} {a : α✝} {i : Nat} : (replicate n a).setIfInBounds i a = replicate n a

@[simp]

theorem Vector.replicate_append_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} : replicate n a ++ replicate m a = replicate (n + m) a

theorem Vector.append_eq_replicate_iff {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {a : α} : xs ++ ys = replicate (n + m) a ↔ xs = replicate n a ∧ ys = replicate m a

theorem Vector.replicate_eq_append_iff {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {a : α} : replicate (n + m) a = xs ++ ys ↔ xs = replicate n a ∧ ys = replicate m a

@[simp]

theorem Vector.map_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : map f (replicate n a) = replicate n (f a)

@[simp]

theorem Vector.flatten_replicate_empty {n : Nat} {α : Type u_1} : (replicate n #v[]).flatten = #v[]

@[simp]

theorem Vector.flatten_replicate_singleton {n : Nat} {α✝ : Type u_1} {a : α✝} : (replicate n #v[a]).flatten = Vector.cast ⋯ (replicate n a)

@[simp]

theorem Vector.flatten_replicate_replicate {n m : Nat} {α✝ : Type u_1} {a : α✝} : (replicate n (replicate m a)).flatten = replicate (n * m) a

theorem Vector.flatMap_replicate {α : Type u_1} {β : Type u_2} {m n : Nat} {a : α} {f : α → Vector β m} : (replicate n a).flatMap f = (replicate n (f a)).flatten

reverse

theorem Vector.reverse_empty {α : Type u_1} : #v[].reverse = #v[]

@[simp]

theorem Vector.reverse_push {α : Type u_1} {n : Nat} {as : Vector α n} {a : α} : (as.push a).reverse = Vector.cast ⋯ (#v[a] ++ as.reverse)

@[simp]

theorem Vector.mem_reverse {α : Type u_1} {n : Nat} {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as

@[simp]

theorem Vector.getElem_reverse {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (hi : i < n) : xs.reverse[i] = xs[n - 1 - i]

theorem Vector.getElem_eq_getElem_reverse {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs[i] = xs.reverse[n - 1 - i]

theorem Vector.getElem?_reverse' {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (h : i + j + 1 = n) : xs.reverse[i]? = xs[j]?

Variant of getElem?_reverse with a hypothesis giving the linear relation between the indices.

@[simp]

theorem Vector.getElem?_reverse {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs.reverse[i]? = xs[n - 1 - i]?

@[simp]

theorem Vector.reverse_reverse {α : Type u_1} {n : Nat} (xs : Vector α n) : xs.reverse.reverse = xs

theorem Vector.reverse_eq_iff {α : Type u_1} {n : Nat} {xs ys : Vector α n} : xs.reverse = ys ↔ xs = ys.reverse

@[simp]

theorem Vector.reverse_inj {α : Type u_1} {n : Nat} {xs ys : Vector α n} : xs.reverse = ys.reverse ↔ xs = ys

@[simp]

theorem Vector.reverse_eq_push_iff {α : Type u_1} {n : Nat} {xs : Vector α (n + 1)} {ys : Vector α n} {a : α} : xs.reverse = ys.push a ↔ xs = Vector.cast ⋯ (#v[a] ++ ys.reverse)

@[simp]

theorem Vector.map_reverse {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {xs : Vector α n} : map f xs.reverse = (map f xs).reverse

@[simp]

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

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

@[simp]

theorem Vector.reverse_eq_append_iff {α : Type u_1} {n m : Nat} {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m} : xs.reverse = ys ++ zs ↔ xs = Vector.cast ⋯ (zs.reverse ++ ys.reverse)

theorem Vector.reverse_flatten {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} : xss.flatten.reverse = (map reverse xss).reverse.flatten

Reversing a flatten is the same as reversing the order of parts and reversing all parts.

theorem Vector.flatten_reverse {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} : xss.reverse.flatten = (map reverse xss).flatten.reverse

Flattening a reverse is the same as reversing all parts and reversing the flattened result.

theorem Vector.reverse_flatMap {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} : (xs.flatMap f).reverse = xs.reverse.flatMap (reverse ∘ f)

theorem Vector.flatMap_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} : xs.reverse.flatMap f = (xs.flatMap (reverse ∘ f)).reverse

@[simp]

theorem Vector.reverse_replicate {α : Type u_1} {n : Nat} {a : α} : (replicate n a).reverse = replicate n a

extract

@[simp]

theorem Vector.getElem_extract {α : Type u_1} {n i : Nat} {as : Vector α n} {start stop : Nat} (h : i < min stop n - start) : (as.extract start stop)[i] = as[start + i]

theorem Vector.getElem?_extract {α : Type u_1} {n i : Nat} {as : Vector α n} {start stop : Nat} : (as.extract start stop)[i]? = if i < min stop n - start then as[start + i]? else none

@[simp]

theorem Vector.extract_size {α : Type u_1} {n : Nat} {as : Vector α n} : as.extract = Vector.cast ⋯ as

theorem Vector.extract_empty {α : Type u_1} {start stop : Nat} : #v[].extract start stop = Vector.cast ⋯ #v[]

foldlM and foldrM

@[simp]

theorem Vector.foldlM_append {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n k : Nat} [Monad m] [LawfulMonad m] {f : β → α → m β} {b : β} {xs : Vector α n} {ys : Vector α k} : foldlM f b (xs ++ ys) = do let b ← foldlM f b xs foldlM f b ys

theorem Vector.foldlM_empty {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] {f : β → α → m β} {init : β} : foldlM f init #v[] = pure init

theorem Vector.foldrM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → β → m β} {init : β} : foldrM f init #v[] = pure init

@[simp]

theorem Vector.foldlM_push {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β → α → m β} {b : β} : foldlM f b (xs.push a) = do let b ← foldlM f b xs f b a

@[simp]

theorem Vector.foldlM_pure {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} [Monad m] [LawfulMonad m] {f : β → α → β} {b : β} {xs : Vector α n} : foldlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) b xs = pure (foldl f b xs)

@[simp]

theorem Vector.foldrM_pure {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : α → β → β} {b : β} {xs : Vector α n} : foldrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) b xs = pure (foldr f b xs)

theorem Vector.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} {n : Nat} {f : β → α → β} {b : β} {xs : Vector α n} : foldl f b xs = (foldlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) b xs).run

theorem Vector.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β → β} {b : β} {xs : Vector α n} : foldr f b xs = (foldrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) b xs).run

@[simp]

theorem Vector.idRun_foldlM {β : Type u_1} {α : Type u_2} {n : Nat} {f : β → α → Id β} {b : β} {xs : Vector α n} : (foldlM f b xs).run = foldl (fun (x1 : β) (x2 : α) => (f x1 x2).run) b xs

@[simp]

theorem Vector.idRun_foldrM {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β → Id β} {b : β} {xs : Vector α n} : (foldrM f b xs).run = foldr (fun (x1 : α) (x2 : β) => (f x1 x2).run) b xs

@[simp]

theorem Vector.foldlM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] {xs : Vector α n} {f : β → α → m β} {b : β} : foldlM f b xs.reverse = foldrM (fun (x : α) (y : β) => f y x) b xs

@[simp]

theorem Vector.foldrM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] {xs : Vector α n} {f : α → β → m β} {b : β} : foldrM f b xs.reverse = foldlM (fun (x : β) (y : α) => f y x) b xs

@[simp]

theorem Vector.foldrM_push {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] {f : α → β → m β} {init : β} {xs : Vector α n} {a : α} : foldrM f init (xs.push a) = do let b ← f a init foldrM f b xs

foldl / foldr

theorem Vector.foldl_empty {β : Type u_1} {α : Type u_2} {f : β → α → β} {init : β} : foldl f init #v[] = init

theorem Vector.foldr_empty {α : Type u_1} {β : Type u_2} {f : α → β → β} {init : β} : foldr f init #v[] = init

theorem Vector.foldl_congr {α : Type u_1} {n : Nat} {β : Type u_2} {xs ys : Vector α n} (h₀ : xs = ys) {f g : β → α → β} (h₁ : f = g) {a b : β} (h₂ : a = b) : foldl f a xs = foldl g b ys

theorem Vector.foldr_congr {α : Type u_1} {n : Nat} {β : Type u_2} {xs ys : Vector α n} (h₀ : xs = ys) {f g : α → β → β} (h₁ : f = g) {a b : β} (h₂ : a = b) : foldr f a xs = foldr g b ys

@[simp]

theorem Vector.foldl_push {β : Type u_1} {α : Type u_2} {n : Nat} {f : β → α → β} {init : β} {xs : Vector α n} {a : α} : foldl f init (xs.push a) = f (foldl f init xs) a

@[simp]

theorem Vector.foldr_push {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β → β} {init : β} {xs : Vector α n} {a : α} : foldr f init (xs.push a) = foldr f (f a init) xs

theorem Vector.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {n : Nat} {f : β₁ → β₂} {g : α → β₂ → α} {xs : Vector β₁ n} {init : α} : foldl g init (map f xs) = foldl (fun (x : α) (y : β₁) => g x (f y)) init xs

theorem Vector.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {n : Nat} {f : α₁ → α₂} {g : α₂ → β → β} {xs : Vector α₁ n} {init : β} : foldr g init (map f xs) = foldr (fun (x : α₁) (y : β) => g (f x) y) init xs

theorem Vector.foldl_flatMap {α : Type u_1} {β : Type u_2} {m : Nat} {γ : Type u_3} {n : Nat} {f : α → Vector β m} {g : γ → β → γ} {xs : Vector α n} {init : γ} : foldl g init (xs.flatMap f) = foldl (fun (acc : γ) (x : α) => foldl g acc (f x)) init xs

theorem Vector.foldr_flatMap {α : Type u_1} {β : Type u_2} {m : Nat} {γ : Type u_3} {n : Nat} {f : α → Vector β m} {g : β → γ → γ} {xs : Vector α n} {init : γ} : foldr g init (xs.flatMap f) = foldr (fun (x : α) (acc : γ) => foldr g acc (f x)) init xs

theorem Vector.foldl_map_hom {α : Type u_1} {β : Type u_2} {n : Nat} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Vector α n} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : foldl f' (g a) (map g xs) = g (foldl f a xs)

theorem Vector.foldr_map_hom {α : Type u_1} {β : Type u_2} {n : Nat} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Vector α n} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : foldr f' (g a) (map g xs) = g (foldr f a xs)

@[simp]

theorem Vector.foldrM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n k : Nat} [Monad m] [LawfulMonad m] {f : α → β → m β} {b : β} {xs : Vector α n} {ys : Vector α k} : foldrM f b (xs ++ ys) = do let b ← foldrM f b ys foldrM f b xs

@[simp]

theorem Vector.foldl_append {α : Type u_1} {n k : Nat} {β : Type u_2} {f : β → α → β} {b : β} {xs : Vector α n} {ys : Vector α k} : foldl f b (xs ++ ys) = foldl f (foldl f b xs) ys

@[simp]

theorem Vector.foldr_append {α : Type u_1} {β : Type u_2} {n k : Nat} {f : α → β → β} {b : β} {xs : Vector α n} {ys : Vector α k} : foldr f b (xs ++ ys) = foldr f (foldr f b ys) xs

@[simp]

theorem Vector.foldl_flatten {β : Type u_1} {α : Type u_2} {m n : Nat} {f : β → α → β} {b : β} {xss : Vector (Vector α m) n} : foldl f b xss.flatten = foldl (fun (b : β) (xs : Vector α m) => foldl f b xs) b xss

@[simp]

theorem Vector.foldr_flatten {α : Type u_1} {β : Type u_2} {m n : Nat} {f : α → β → β} {b : β} {xss : Vector (Vector α m) n} : foldr f b xss.flatten = foldr (fun (xs : Vector α m) (b : β) => foldr f b xs) b xss

@[simp]

theorem Vector.foldl_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : β → α → β} {b : β} : foldl f b xs.reverse = foldr (fun (x : α) (y : β) => f y x) b xs

@[simp]

theorem Vector.foldr_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : α → β → β} {b : β} : foldr f b xs.reverse = foldl (fun (x : β) (y : α) => f y x) b xs

theorem Vector.foldl_eq_foldr_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : β → α → β} {b : β} : foldl f b xs = foldr (fun (x : α) (y : β) => f y x) b xs.reverse

theorem Vector.foldr_eq_foldl_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : α → β → β} {b : β} : foldr f b xs = foldl (fun (x : β) (y : α) => f y x) b xs.reverse

theorem Vector.foldl_assoc {α : Type u_1} {n : Nat} {op : α → α → α} [ha : Std.Associative op] {xs : Vector α n} {a₁ a₂ : α} : foldl op (op a₁ a₂) xs = op a₁ (foldl op a₂ xs)

@[simp]

theorem Vector.foldr_assoc {α : Type u_1} {n : Nat} {op : α → α → α} [ha : Std.Associative op] {xs : Vector α n} {a₁ a₂ : α} : foldr op (op a₁ a₂) xs = op (foldr op a₁ xs) a₂

theorem Vector.foldl_hom {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {n : Nat} (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {xs : Vector β n} {init : α₁} (H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) : foldl g₂ (f init) xs = f (foldl g₁ init xs)

theorem Vector.foldr_hom {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {n : Nat} (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ : α → β₂ → β₂} {xs : Vector α n} {init : β₁} (H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) : foldr g₂ (f init) xs = f (foldr g₁ init xs)

theorem Vector.foldl_rel {α : Type u_1} {n : Nat} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop} (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) : r (foldl (fun (acc : β) (a : α) => f acc a) a xs) (foldl (fun (acc : γ) (a : α) => g acc a) b xs)

We can prove that two folds over the same vector are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the vector, preserves the relation.

theorem Vector.foldr_rel {α : Type u_1} {n : Nat} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop} (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) : r (foldr (fun (a : α) (acc : β) => f a acc) a xs) (foldr (fun (a : α) (acc : γ) => g a acc) b xs)

We can prove that two folds over the same vector are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the vector, preserves the relation.

@[simp]

theorem Vector.foldl_add_const {α : Type u_1} {n : Nat} {xs : Vector α n} {a b : Nat} : foldl (fun (x : Nat) (x_1 : α) => x + a) b xs = b + a * n

@[simp]

theorem Vector.foldr_add_const {α : Type u_1} {n : Nat} {xs : Vector α n} {a b : Nat} : foldr (fun (x : α) (x_1 : Nat) => x_1 + a) b xs = b + a * n

Further results about back and back?

@[simp]

theorem Vector.back?_eq_none_iff {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.back? = none ↔ n = 0

theorem Vector.back?_eq_some_iff {α : Type u_1} {n : Nat} {xs : Vector α n} {a : α} : xs.back? = some a ↔ ∃ (w : 0 < n), ∃ (ys : Vector α (n - 1)), xs = Vector.cast ⋯ (ys.push a)

@[simp]

theorem Vector.back?_isSome {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.back?.isSome = true ↔ n ≠ 0

@[simp]

theorem Vector.back_append_of_neZero {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} [NeZero m] : (xs ++ ys).back = ys.back

theorem Vector.back_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} [NeZero (n + m)] : (xs ++ ys).back = if h' : m = 0 then have this := ⋯; xs.back else have this := ⋯; ys.back

theorem Vector.back_append_right {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} [NeZero m] : (xs ++ ys).back = ys.back

theorem Vector.back_append_left {α : Type u_1} {n : Nat} {xs : Vector α n} {ys : Vector α 0} [NeZero n] : (xs ++ ys).back = xs.back

@[simp]

theorem Vector.back?_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back?

theorem Vector.back?_flatMap {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} : (xs.flatMap f).back? = findSome? (fun (a : α) => (f a).back?) xs.reverse

theorem Vector.back?_flatten {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} : xss.flatten.back? = findSome? (fun (xs : Vector α m) => xs.back?) xss.reverse

theorem Vector.back?_replicate {α : Type u_1} {a : α} {n : Nat} : (replicate n a).back? = if n = 0 then none else some a

@[simp]

theorem Vector.back_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} [NeZero n] : (replicate n a).back = a

leftpad and rightpad

@[simp]

theorem Vector.leftpad_mk {α : Type u_1} {m n : Nat} {a : α} {xs : Array α} (h : xs.size = m) : leftpad n a (mk xs h) = mk (Array.leftpad n a xs) ⋯

@[simp]

theorem Vector.rightpad_mk {α : Type u_1} {m n : Nat} {a : α} {xs : Array α} (h : xs.size = m) : rightpad n a (mk xs h) = mk (Array.rightpad n a xs) ⋯

contains

theorem Vector.contains_eq_any_beq {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {a : α} : xs.contains a = xs.any fun (x : α) => a == x

theorem Vector.contains_iff_exists_mem_beq {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {a : α} : xs.contains a = true ↔ ∃ (a' : α), a' ∈ xs ∧ (a == a') = true

@[simp]

theorem Vector.contains_toList {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {x : α} : xs.toList.contains x = xs.contains x

@[simp]

theorem Vector.contains_toArray {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {x : α} : xs.toArray.contains x = xs.contains x

@[simp]

theorem Vector.contains_map {β : Type u_1} {α : Type u_2} {n : Nat} [BEq β] {xs : Vector α n} {x : β} {f : α → β} : (map f xs).contains x = xs.any fun (a : α) => x == f a

@[simp]

theorem Vector.contains_append {α : Type u_1} {n m : Nat} [BEq α] {xs : Vector α n} {ys : Vector α m} {x : α} : (xs ++ ys).contains x = (xs.contains x || ys.contains x)

@[simp]

theorem Vector.contains_flatten {α : Type u_1} {n m : Nat} [BEq α] {xs : Vector (Vector α n) m} {x : α} : xs.flatten.contains x = xs.any fun (xs : Vector α n) => xs.contains x

@[simp]

theorem Vector.contains_reverse {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {x : α} : xs.reverse.contains x = xs.contains x

@[simp]

theorem Vector.contains_flatMap {β : Type u_1} {α : Type u_2} {n m : Nat} [BEq β] {xs : Vector α n} {f : α → Vector β m} {x : β} : (xs.flatMap f).contains x = xs.any fun (a : α) => (f a).contains x

more lemmas about pop

@[simp]

theorem Vector.pop_empty {α : Type u_1} : #v[].pop = #v[]

@[simp]

theorem Vector.pop_push {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} : (xs.push x).pop = xs

@[simp]

theorem Vector.getElem_pop {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n - 1) : xs.pop[i] = xs[i]

@[simp]

theorem Vector.getElem_pop' {α : Type u_1} {n : Nat} {xs : Vector α (n + 1)} {i : Nat} (h : i < n + 1 - 1) : xs.pop[i] = xs[i]

Variant of getElem_pop that will sometimes fire when getElem_pop gets stuck because of defeq issues in the implicit size argument.

theorem Vector.getElem?_pop {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : xs.pop[i]? = if i < n - 1 then xs[i]? else none

theorem Vector.back_pop {α : Type u_1} {n : Nat} {xs : Vector α n} [h : NeZero (n - 1)] : xs.pop.back = xs[n - 2]

theorem Vector.back?_pop {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.pop.back? = if n ≤ 1 then none else xs[n - 2]?

@[simp]

theorem Vector.pop_append_of_size_ne_zero {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} (h : m ≠ 0) : (xs ++ ys).pop = Vector.cast ⋯ (xs ++ ys.pop)

theorem Vector.pop_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).pop = if h : m = 0 then Vector.cast ⋯ xs.pop else Vector.cast ⋯ (xs ++ ys.pop)

@[simp]

theorem Vector.pop_replicate {α : Type u_1} {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a

Logic

any / all

theorem Vector.not_any_eq_all_not {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : (!xs.any p) = xs.all fun (a : α) => !p a

theorem Vector.not_all_eq_any_not {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : (!xs.all p) = xs.any fun (a : α) => !p a

theorem Vector.and_any_distrib_left {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} {q : Bool} : (q && xs.any p) = xs.any fun (a : α) => q && p a

theorem Vector.and_any_distrib_right {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} {q : Bool} : (xs.any p && q) = xs.any fun (a : α) => p a && q

theorem Vector.or_all_distrib_left {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} {q : Bool} : (q || xs.all p) = xs.all fun (a : α) => q || p a

theorem Vector.or_all_distrib_right {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} {q : Bool} : (xs.all p || q) = xs.all fun (a : α) => p a || q

theorem Vector.any_eq_not_all_not {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : xs.any p = !xs.all fun (x : α) => !p x

@[simp]

theorem Vector.any_map {α : Type u_1} {n : Nat} {β : Type u_2} {f : α → β} {xs : Vector α n} {p : β → Bool} : (map f xs).any p = xs.any (p ∘ f)

@[simp]

theorem Vector.all_map {α : Type u_1} {n : Nat} {β : Type u_2} {f : α → β} {xs : Vector α n} {p : β → Bool} : (map f xs).all p = xs.all (p ∘ f)

@[simp]

theorem Vector.any_append {α : Type u_1} {n m : Nat} {f : α → Bool} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).any f = (xs.any f || ys.any f)

@[simp]

theorem Vector.all_append {α : Type u_1} {n m : Nat} {f : α → Bool} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).all f = (xs.all f && ys.all f)

theorem Vector.anyM_congr {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] {xs ys : Vector α n} (w : xs = ys) {p q : α → m Bool} (h : ∀ (a : α), p a = q a) : anyM p xs = anyM q ys

theorem Vector.any_congr {α : Type u_1} {n : Nat} {xs ys : Vector α n} (w : xs = ys) {p q : α → Bool} (h : ∀ (a : α), p a = q a) : xs.any p = ys.any q

theorem Vector.allM_congr {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] {xs ys : Vector α n} (w : xs = ys) {p q : α → m Bool} (h : ∀ (a : α), p a = q a) : allM p xs = allM q ys

theorem Vector.all_congr {α : Type u_1} {n : Nat} {xs ys : Vector α n} (w : xs = ys) {p q : α → Bool} (h : ∀ (a : α), p a = q a) : xs.all p = ys.all q

@[simp]

theorem Vector.any_flatten {α : Type u_1} {n m : Nat} {f : α → Bool} {xss : Vector (Vector α n) m} : xss.flatten.any f = xss.any fun (x : Vector α n) => x.any f

@[simp]

theorem Vector.all_flatten {α : Type u_1} {n m : Nat} {f : α → Bool} {xss : Vector (Vector α n) m} : xss.flatten.all f = xss.all fun (x : Vector α n) => x.all f

@[simp]

theorem Vector.any_flatMap {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} : (xs.flatMap f).any p = xs.any fun (a : α) => (f a).any p

@[simp]

theorem Vector.all_flatMap {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} : (xs.flatMap f).all p = xs.all fun (a : α) => (f a).all p

@[simp]

theorem Vector.any_reverse {α : Type u_1} {n : Nat} {f : α → Bool} {xs : Vector α n} : xs.reverse.any f = xs.any f

@[simp]

theorem Vector.all_reverse {α : Type u_1} {n : Nat} {f : α → Bool} {xs : Vector α n} : xs.reverse.all f = xs.all f

@[simp]

theorem Vector.any_cast {α : Type u_1} {n a✝ : Nat} {h : n = a✝} {f : α → Bool} {xs : Vector α n} : (Vector.cast h xs).any f = xs.any f

@[simp]

theorem Vector.all_cast {α : Type u_1} {n a✝ : Nat} {h : n = a✝} {f : α → Bool} {xs : Vector α n} : (Vector.cast h xs).all f = xs.all f

@[simp]

theorem Vector.any_replicate {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (replicate n a).any f = if n = 0 then false else f a

@[simp]

theorem Vector.all_replicate {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (replicate n a).all f = if n = 0 then true else f a

replace

@[simp]

theorem Vector.replace_cast {α : Type u_1} [BEq α] {n m : Nat} {h : n = m} {xs : Vector α n} {a b : α} : (Vector.cast h xs).replace a b = Vector.cast ⋯ (xs.replace a b)

@[simp]

theorem Vector.replace_empty {α : Type u_1} [BEq α] {a b : α} : #v[].replace a b = #v[]

theorem Vector.replace_singleton {α : Type u_1} [BEq α] {a b c : α} : #v[a].replace b c = #v[if (a == b) = true then c else a]

@[simp]

theorem Vector.replace_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} {xs : Vector α n} (h : ¬a ∈ xs) : xs.replace a b = xs

theorem Vector.getElem?_replace {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} {xs : Vector α n} {i : Nat} : (xs.replace a b)[i]? = if (xs[i]? == some a) = true then if a ∈ xs.take i then some a else some b else xs[i]?

theorem Vector.getElem?_replace_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) : (xs.replace a b)[i]? = xs[i]?

theorem Vector.getElem_replace {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} {xs : Vector α n} {i : Nat} (h : i < n) : (xs.replace a b)[i] = if (xs[i] == a) = true then if a ∈ xs.take i then a else b else xs[i]

theorem Vector.getElem_replace_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) : (xs.replace a b)[i] = xs[i]

theorem Vector.replace_append {α : Type u_1} [BEq α] [LawfulBEq α] {n m : Nat} {a b : α} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b

theorem Vector.replace_append_left {α : Type u_1} [BEq α] [LawfulBEq α] {n m : Nat} {a b : α} {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) : (xs ++ ys).replace a b = xs.replace a b ++ ys

theorem Vector.replace_append_right {α : Type u_1} [BEq α] [LawfulBEq α] {n m : Nat} {a b : α} {xs : Vector α n} {ys : Vector α m} (h : ¬a ∈ xs) : (xs ++ ys).replace a b = xs ++ ys.replace a b

theorem Vector.replace_push {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {xs : Vector α n} {a b c : α} : (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if (b == a) = true then c else a)

theorem Vector.replace_extract {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} {xs : Vector α n} {i : Nat} : (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i

@[simp]

theorem Vector.replace_replicate_self {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {b a : α} (h : 0 < n) : (replicate n a).replace a b = Vector.cast ⋯ (#v[b] ++ replicate (n - 1) a)

@[simp]

theorem Vector.replace_replicate_ne {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b c : α} (h : (!b == a) = true) : (replicate n a).replace b c = replicate n a

Content below this point has not yet been aligned with List and Array.

theorem Vector.getElem_push_last {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α} : (xs.push x)[n] = x

@[simp]

theorem Vector.push_pop_back {α : Type u_1} {n : Nat} (xs : Vector α (n + 1)) : xs.pop.push xs.back = xs

findRev? and findSomeRev?

@[simp]

theorem Vector.findRev?_eq_find?_reverse {α : Type} {n : Nat} {f : α → Bool} {xs : Vector α n} : findRev? f xs = find? f xs.reverse

@[simp]

theorem Vector.findSomeRev?_eq_findSome?_reverse {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} : findSomeRev? f xs = findSome? f xs.reverse

zipWith

@[simp]

theorem Vector.getElem_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β → γ} {as : Vector α n} {bs : Vector β n} {i : Nat} (hi : i < n) : (zipWith f as bs)[i] = f as[i] bs[i]

take

theorem Vector.take_size {α : Type u_1} {n : Nat} {as : Vector α n} : as.take n = Vector.cast ⋯ as

swap

theorem Vector.getElem_swap {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (hi : i < n) (hj : j < n) {k : Nat} (hk : k < n) : (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]

@[simp]

theorem Vector.getElem_swap_right {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (hi : i < n) (hj : j < n) : (xs.swap i j hi hj)[j] = xs[i]

@[simp]

theorem Vector.getElem_swap_left {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (hi : i < n) (hj : j < n) : (xs.swap i j hi hj)[i] = xs[j]

@[simp]

theorem Vector.getElem_swap_of_ne {α : Type u_1} {n k : Nat} {xs : Vector α n} {i j : Nat} {hi : i < n} {hj : j < n} {hk : k < n} (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k] = xs[k]

theorem Vector.getElem?_swap {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (hi : i < n) (hj : j < n) {k : Nat} : (xs.swap i j hi hj)[k]? = if j = k then some xs[i] else if i = k then some xs[j] else xs[k]?

@[simp]

theorem Vector.swap_swap {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (hi : i < n) (hj : j < n) : (xs.swap i j hi hj).swap i j hi hj = xs

theorem Vector.swap_comm {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (hi : i < n) (hj : j < n) : xs.swap i j hi hj = xs.swap j i hj hi

take

@[simp]

theorem Vector.getElem_take {α : Type u_1} {n i : Nat} {xs : Vector α n} {j : Nat} (hi : i < min j n) : (xs.take j)[i] = xs[i]

drop

theorem Vector.getElem_drop {α : Type u_1} {n i : Nat} {xs : Vector α n} {j : Nat} (hi : i < n - j) : (xs.drop j)[i] = xs[j + i]

Decidable quantifiers.

theorem Vector.forall_zero_iff {α : Type u_1} {P : Vector α 0 → Prop} : (∀ (xs : Vector α 0), P xs) ↔ P #v[]

theorem Vector.forall_cons_iff {α : Type u_1} {n : Nat} {P : Vector α (n + 1) → Prop} : (∀ (xs : Vector α (n + 1)), P xs) ↔ ∀ (x : α) (xs : Vector α n), P (xs.push x)

@[implicit_reducible]

instance Vector.instDecidableForallVectorZero {α : Type u_1} (P : Vector α 0 → Prop) [Decidable (P #v[])] : Decidable (∀ (xs : Vector α 0), P xs)

Equations

• Vector.instDecidableForallVectorZero P = isTrue ⋯
• Vector.instDecidableForallVectorZero P = isFalse ⋯

@[implicit_reducible]

instance Vector.instDecidableForallVectorSucc {α : Type u_1} {n : Nat} (P : Vector α (n + 1) → Prop) [Decidable (∀ (x : α) (xs : Vector α n), P (xs.push x))] : Decidable (∀ (xs : Vector α (n + 1)), P xs)

Equations

• Vector.instDecidableForallVectorSucc P = decidable_of_iff' (∀ (x : α) (xs : Vector α n), P (xs.push x)) ⋯

@[implicit_reducible]

instance Vector.instDecidableExistsVectorZero {α : Type u_1} (P : Vector α 0 → Prop) [Decidable (P #v[])] : Decidable (∃ (xs : Vector α 0), P xs)

Equations

• Vector.instDecidableExistsVectorZero P = decidable_of_iff (¬∀ (xs : Vector α 0), ¬P xs) ⋯

@[implicit_reducible]

instance Vector.instDecidableExistsVectorSucc {α : Type u_1} {n : Nat} (P : Vector α (n + 1) → Prop) [Decidable (∀ (x : α) (xs : Vector α n), ¬P (xs.push x))] : Decidable (∃ (xs : Vector α (n + 1)), P xs)

Equations

• Vector.instDecidableExistsVectorSucc P = decidable_of_iff (¬∀ (xs : Vector α (n + 1)), ¬P xs) ⋯

sum

@[simp]

theorem Vector.sum_empty {α : Type u_1} [Add α] [Zero α] : #v[].sum = 0

theorem Vector.sum_eq_foldr {α : Type u_1} {n : Nat} [Add α] [Zero α] {xs : Vector α n} : xs.sum = foldr (fun (x1 x2 : α) => x1 + x2) 0 xs

@[simp]

theorem Vector.sum_append {α : Type u_1} {n : Nat} [Zero α] [Add α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LeftIdentity (fun (x1 x2 : α) => x1 + x2) 0] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 + x2) 0] {as₁ as₂ : Vector α n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum

@[simp]

theorem Vector.sum_reverse {α : Type u_1} {n : Nat} [Zero α] [Add α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.Commutative fun (x1 x2 : α) => x1 + x2] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 + x2) 0] (xs : Vector α n) : xs.reverse.sum = xs.sum