Vectors

Lemmas about Vector α n

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

mk lemmas

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

@[simp]

theorem Vector.mk_toArray {α : Type u_1} {n : Nat} (v : Vector α n) : { toArray := v.toArray, size_toArray := ⋯ } = v

@[simp]

theorem Vector.getElem_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) : { toArray := data, size_toArray := size }[i] = data[i]

@[simp]

theorem Vector.getElem?_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} {i : Nat} : { toArray := data, size_toArray := size }[i]? = data[i]?

@[simp]

theorem Vector.mem_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} {a : α} : a ∈ { toArray := data, size_toArray := size } ↔ a ∈ data

@[simp]

theorem Vector.contains_mk {α : Type u_1} {n : Nat} [BEq α] {data : Array α} {size : data.size = n} {a : α} : { toArray := data, size_toArray := size }.contains a = data.contains a

@[simp]

theorem Vector.push_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} {x : α} : { toArray := data, size_toArray := size }.push x = { toArray := data.push x, size_toArray := ⋯ }

@[simp]

theorem Vector.pop_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} : { toArray := data, size_toArray := size }.pop = { toArray := data.pop, size_toArray := ⋯ }

@[simp]

theorem Vector.mk_beq_mk {α : Type u_1} {n : Nat} [BEq α] {a b : Array α} {h : a.size = n} {h' : b.size = n} : ({ toArray := a, size_toArray := h } == { toArray := b, size_toArray := h' }) = (a == b)

@[simp]

theorem Vector.allDiff_mk {α : Type u_1} {n : Nat} [BEq α] (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.allDiff = a.allDiff

@[simp]

theorem Vector.mk_append_mk {α : Type u_1} {n m : Nat} (a b : Array α) (ha : a.size = n) (hb : b.size = m) : { toArray := a, size_toArray := ha } ++ { toArray := b, size_toArray := hb } = { toArray := a ++ b, size_toArray := ⋯ }

@[simp]

theorem Vector.back!_mk {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.back! = a.back!

@[simp]

theorem Vector.back?_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.back? = a.back?

@[simp]

theorem Vector.back_mk {n : Nat} {α : Type u_1} [NeZero n] (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.back = a[n - 1]

@[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 : β) (a : Array α) (h : a.size = n) : foldlM f b { toArray := a, size_toArray := h } = Array.foldlM f b a

@[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 : β) (a : Array α) (h : a.size = n) : foldrM f b { toArray := a, size_toArray := h } = Array.foldrM f b a

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.drop_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (m : Nat) : { toArray := a, size_toArray := h }.drop m = { toArray := a.extract m, size_toArray := ⋯ }

@[simp]

theorem Vector.eraseIdx_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (h' : i < n) : { toArray := a, size_toArray := h }.eraseIdx i h' = { toArray := a.eraseIdx i ⋯, size_toArray := ⋯ }

@[simp]

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

@[simp]

theorem Vector.cast_mk {α : Type u_1} {n m : Nat} (a : Array α) (h : a.size = n) (h' : n = m) : Vector.cast h' { toArray := a, size_toArray := h } = { toArray := a, size_toArray := ⋯ }

@[simp]

theorem Vector.extract_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (start stop : Nat) : { toArray := a, size_toArray := h }.extract start stop = { toArray := a.extract start stop, size_toArray := ⋯ }

@[simp]

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

@[simp]

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

@[reducible, inline, deprecated Vector.finIdxOf?_mk (since := "2025-01-29")]

abbrev Vector.indexOf?_mk {α : Type u_1} {n : Nat} [BEq α] (a : Array α) (h : a.size = n) (x : α) : { toArray := a, size_toArray := h }.finIdxOf? x = Option.map (Fin.cast h) (a.finIdxOf? x)

Equations

• @Vector.indexOf?_mk = @Vector.finIdxOf?_mk

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.find?_mk {α : Type} {n : Nat} (a : Array α) (h : a.size = n) (f : α → Bool) : find? f { toArray := a, size_toArray := h } = Array.find? f a

@[simp]

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

@[simp]

theorem Vector.findRev?_mk {α : Type} {n : Nat} (a : Array α) (h : a.size = n) (f : α → Bool) : findRev? f { toArray := a, size_toArray := h } = Array.findRev? f a

@[simp]

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

@[simp]

theorem Vector.mk_isEqv_mk {α : Type u_1} {n : Nat} (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) : { toArray := a, size_toArray := ha }.isEqv { toArray := b, size_toArray := hb } r = a.isEqv b r

@[simp]

theorem Vector.mk_isPrefixOf_mk {α : Type u_1} {n m : Nat} [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = m) : { toArray := a, size_toArray := ha }.isPrefixOf { toArray := b, size_toArray := hb } = a.isPrefixOf b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.forM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} [Monad m] (f : α → m PUnit) (a : Array α) (h : a.size = n) : forM { toArray := a, size_toArray := h } f = forM a 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 ∈ { toArray := xs, size_toArray := h } → β → m (ForInStep β)) : forIn' { toArray := xs, size_toArray := 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} {n : Nat} {β : Type u_1} [Monad m] (xs : Array α) (h : xs.size = n) (b : β) (f : α → β → m (ForInStep β)) : forIn { toArray := xs, size_toArray := h } b f = forIn xs b f

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.reverse_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.reverse = { toArray := a.reverse, size_toArray := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.swapIfInBounds_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) : { toArray := a, size_toArray := h }.swapIfInBounds i j = { toArray := a.swapIfInBounds i j, size_toArray := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.take_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (m : Nat) : { toArray := a, size_toArray := h }.take m = { toArray := a.take m, size_toArray := ⋯ }

@[simp]

theorem Vector.zipIdx_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (k : Nat := 0) : { toArray := a, size_toArray := h }.zipIdx k = { toArray := a.zipIdx k, size_toArray := ⋯ }

@[reducible, inline, deprecated Vector.zipIdx_mk (since := "2025-01-21")]

abbrev Vector.zipWithIndex_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (k : Nat := 0) : { toArray := a, size_toArray := h }.zipIdx k = { toArray := a.zipIdx k, size_toArray := ⋯ }

Equations

• @Vector.zipWithIndex_mk = @Vector.zipIdx_mk

@[simp]

theorem Vector.mk_zipWith_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} (f : α → β → γ) (a : Array α) (b : Array β) (ha : a.size = n) (hb : b.size = n) : zipWith f { toArray := a, size_toArray := ha } { toArray := b, size_toArray := hb } = { toArray := Array.zipWith f a b, size_toArray := ⋯ }

@[simp]

theorem Vector.mk_zip_mk {α : Type u_1} {β : Type u_2} {n : Nat} (a : Array α) (b : Array β) (ha : a.size = n) (hb : b.size = n) : { toArray := a, size_toArray := ha }.zip { toArray := b, size_toArray := hb } = { toArray := a.zip b, size_toArray := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.any_mk {α : Type u_1} {n : Nat} (p : α → Bool) (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.any p = a.any p

@[simp]

theorem Vector.all_mk {α : Type u_1} {n : Nat} (p : α → Bool) (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.all p = a.all p

@[simp]

theorem Vector.countP_mk {α : Type u_1} {n : Nat} (p : α → Bool) (a : Array α) (h : a.size = n) : countP p { toArray := a, size_toArray := h } = Array.countP p a

@[simp]

theorem Vector.count_mk {α : Type u_1} {n : Nat} [BEq α] (a : Array α) (h : a.size = n) (b : α) : count b { toArray := a, size_toArray := h } = Array.count b a

@[simp]

theorem Vector.eq_mk {α✝ : Type u_1} {n✝ : Nat} {v : Vector α✝ n✝} {a : Array α✝} {h : a.size = n✝} : v = { toArray := a, size_toArray := h } ↔ v.toArray = a

@[simp]

theorem Vector.mk_eq {α✝ : Type u_1} {a : Array α✝} {a✝ : Nat} {h : a.size = a✝} {v : Vector α✝ a✝} : { toArray := a, size_toArray := h } = v ↔ a = v.toArray

toArray lemmas

@[simp]

theorem Vector.getElem_toArray {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (h : i < xs.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} (a : Vector α m) (b : Vector α n) : (a ++ b).toArray = a.toArray ++ b.toArray

@[simp]

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

@[simp]

theorem Vector.toArray_empty {α : Type u_1} : { toArray := #[], size_toArray := ⋯ }.toArray = #[]

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[irreducible]

theorem Vector.toArray_mapM_go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] (f : α → m β) (v : Vector α n) (i : Nat) (h : i ≤ n) (r : Vector β i) : toArray <$> mapM.go f v i h r = Array.mapM.map f v.toArray i r.toArray

@[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 β) (a : Vector α n) : toArray <$> mapM f a = Array.mapM f a.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} (a : Vector α n) : a.pop.toArray = a.pop

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.toArray_setIfInBounds {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) : (a.setIfInBounds i x).toArray = a.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} (a : Vector α n) (i j : Nat) (hi : j < n) (hj : i < n) : (a.swap i j hj hi).toArray = a.swap i j ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.any_toArray {α : Type u_1} {n : Nat} (p : α → Bool) (v : Vector α n) : v.any p = v.any p

@[simp]

theorem Vector.all_toArray {α : Type u_1} {n : Nat} (p : α → Bool) (v : Vector α n) : v.all p = v.all p

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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 β)) (v : Vector α n) : Array.findSomeM? f v.toArray = findSomeM? f v

@[simp]

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

@[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 β)) (v : Vector α n) : Array.findSomeRevM? f v.toArray = findSomeRevM? f v

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.toArray_mkVector {n : Nat} {α✝ : Type u_1} {a : α✝} : (mkVector n a).toArray = mkArray n a

@[simp]

theorem Vector.toArray_inj {α : Type u_1} {n : Nat} {v w : Vector α n} : v.toArray = w.toArray ↔ v = w

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

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

@[simp]

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

toList

theorem Vector.toArray_toList {α : Type u_1} {n : Nat} (a : Vector α n) : a.toList = a.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]?

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

@[simp]

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

theorem Vector.toList_empty {α : Type u_1} : { toArray := #[], size_toArray := ⋯ }.toArray = #[]

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

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

@[simp]

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

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

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

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

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

theorem Vector.toList_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} (f : (i : Nat) → α → i < n → β) (v : Vector α n) : (v.mapFinIdx f).toList = v.toList.mapFinIdx fun (i : Nat) (a : α) (h : i < v.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} (a : Vector α n) : a.pop.toList = a.toList.dropLast

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

@[simp]

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

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

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

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

@[simp]

theorem Vector.toList_setIfInBounds {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) : (a.setIfInBounds i x).toList = a.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} (a : Vector α n) (i j : Nat) (hi : j < n) (hj : i < n) : (a.swap i j hj hi).toList = (a.toList.set i a[j]).set j a[i]

@[simp]

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

@[simp]

theorem Vector.toList_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} (f : α → β → γ) (a : Vector α n) (b : Vector β n) : (zipWith f a b).toArray = Array.zipWith f a.toArray b.toArray

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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 β)) (v : Vector α n) : List.findSomeM? f v.toList = findSomeM? f v

@[simp]

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

@[simp]

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

@[simp]

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

theorem Vector.toList_inj {α : Type u_1} {n : Nat} {v w : Vector α n} : v.toList = w.toList ↔ v = w

@[simp]

theorem Vector.toList_eq_empty_iff {α : Type u_1} {n : Nat} (v : Vector α n) : v.toList = [] ↔ n = 0

@[simp]

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

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

empty

@[simp]

theorem Vector.empty_eq {α : Type u_1} {xs : Vector α 0} : { toArray := #[], size_toArray := ⋯ } = xs ↔ xs = { toArray := #[], size_toArray := ⋯ }

theorem Vector.eq_empty {α : Type u_1} (v : Vector α 0) : v = { toArray := #[], size_toArray := ⋯ }

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 ⋯ { toArray := #[], size_toArray := ⋯ }

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

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 : α✝} : { toArray := #[a], size_toArray := ⋯ } = { toArray := #[b], size_toArray := ⋯ } ↔ a = b

cast

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

mkVector

@[simp]

theorem Vector.mkVector_zero {α✝ : Type u_1} {a : α✝} : mkVector 0 a = { toArray := #[], size_toArray := ⋯ }

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

@[simp]

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

@[simp]

theorem Array.mk_mkArray {α : Type u_1} {m : Nat} (a : α) (n : Nat) (h : (mkArray n a).size = m) : { toArray := mkArray n a, size_toArray := h } = Vector.cast ⋯ (Vector.mkVector n a)

theorem Vector.mkVector_eq_mk_mkArray {α : Type u_1} (a : α) (n : Nat) : mkVector n a = { toArray := mkArray n a, size_toArray := ⋯ }

L[i] and L[i]?

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

theorem Vector.getElem?_empty {α : Type u_1} {n : Nat} : { toArray := #[], size_toArray := ⋯ }[n]? = none

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem Vector.getElem?_singleton {α : Type u_1} (a : α) (i : Nat) : { toArray := #[a], size_toArray := ⋯ }[i]? = if i = 0 then some a else none

mem

@[simp]

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

@[simp]

theorem Vector.not_mem_empty {α : Type u_1} (a : α) : ¬a ∈ { toArray := #[], size_toArray := ⋯ }

@[simp]

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

theorem Vector.mem_push_self {α : Type u_1} {n : Nat} {a : Vector α n} {x : α} : x ∈ a.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} {a : Vector α n} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.mem_ite_empty_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Vector α 0} : (x ∈ if p then { toArray := #[], size_toArray := ⋯ } else l) ↔ ¬p ∧ x ∈ l

@[simp]

theorem Vector.mem_ite_empty_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Vector α 0} : (x ∈ if p then l else { toArray := #[], size_toArray := ⋯ }) ↔ p ∧ x ∈ l

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

@[simp]

theorem Vector.mem_singleton {α : Type u_1} {a b : α} : a ∈ { toArray := #[b], size_toArray := ⋯ } ↔ 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 : α} {l : Vector α n} : (∀ (a' : α), a' ∈ l → ¬a = a') ↔ ¬a ∈ l

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

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

theorem Vector.forall_mem_empty {α : Type u_1} (p : α → Prop) (x : α) : x ∈ { toArray := #[], size_toArray := ⋯ } → 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 ∈ { toArray := #[a], size_toArray := ⋯ } → p x) ↔ p a

theorem Vector.mem_empty_iff {α : Type u_1} (a : α) : a ∈ { toArray := #[], size_toArray := ⋯ } ↔ False

theorem Vector.mem_singleton_self {α : Type u_1} (a : α) : a ∈ { toArray := #[a], size_toArray := ⋯ }

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

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

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

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

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

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

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

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

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

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

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

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

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 : α} {l : Vector α n} : a ∈ l ↔ ∃ (i : Nat), ∃ (h : i < n), l[i] = a

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

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

Decidability of bounded quantifiers

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]) ⋯

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

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_iff {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} : as.contains a = true ↔ a ∈ as

@[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} [BEq α] {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} [BEq α] {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 α] {l : Vector α n} {a b : α} : (l.push a).contains b = (l.contains b || b == a)

set

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

@[simp]

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

@[reducible, inline, deprecated Vector.getElem_set_self (since := "2024-12-12")]

abbrev Vector.getElem_set_eq {α : Type u_1} {n : Nat} (v : Vector α n) (i : Nat) (x : α) (hi : i < n) : (v.set i x hi)[i] = x

Equations

• @Vector.getElem_set_eq = @Vector.getElem_set_self

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

setIfInBounds

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

@[simp]

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

@[reducible, inline, deprecated Vector.getElem_setIfInBounds_self (since := "2024-12-12")]

abbrev Vector.getElem_setIfInBounds_eq {α : Type u_1} {n : Nat} (v : Vector α n) (i : Nat) (x : α) (hi : i < n) : (v.setIfInBounds i x)[i] = x

Equations

• @Vector.getElem_setIfInBounds_eq = @Vector.getElem_setIfInBounds_self

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem Vector.setIfInBounds_eq_of_size_le {α : Type u_1} {n : Nat} {l : Vector α n} {m : Nat} (h : l.size ≤ m) {a : α} : l.setIfInBounds m a = l

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

@[simp]

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

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

BEq

@[simp]

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

@[simp, irreducible]

theorem Vector.mkVector_beq_mkVector {α : Type u_1} [BEq α] {a b : α} {n : Nat} : (mkVector n a == mkVector 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} [DecidableEq α] {l₁ l₂ : Vector α n} : ((l₁.isEqv l₂ fun (x1 x2 : α) => x1 == x2) = true) = (l₁ = l₂)

map

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) : map f { toArray := #[], size_toArray := ⋯ } = { toArray := #[], size_toArray := ⋯ }

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} (l : Vector α n) : map id l = l

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

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) (l : Vector α n) : map f l = l

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 { toArray := #[a], size_toArray := ⋯ } = { toArray := #[f a], size_toArray := ⋯ }

@[simp]

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

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

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

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

@[simp]

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

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

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

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 : α → β} {l : Vector α (n + 1)} {l₂ : Vector β n} {b : β} : map f l = l₂.push b ↔ ∃ (l₁ : Vector α n), ∃ (a : α), l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.back?_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {l : Vector α n} : (map f l).back? = Option.map f l.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 { toArray := Array.map (fun (x : { x : Array α // x ∈ xss }) => match x with | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ }) xss.attach, size_toArray := ⋯ }) (ass : Vector (Vector α n) m) : P ass

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 → ∀ (x : Array α), x ∈ xs → x.size = n), P { toArray := Array.map (fun (x : { x : Array (Array α) // x ∈ xss }) => match x with | ⟨xs, m_1⟩ => { toArray := Array.map (fun (x : { x : Array α // x ∈ xs }) => match x with | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ }) xs.attach, size_toArray := ⋯ }) xss.attach, size_toArray := ⋯ }) (ass : Vector (Vector (Vector α n) m) k) : P ass

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 = { toArray := #[v], size_toArray := ⋯ }

append

@[simp]

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 : α) : { toArray := #[a], size_toArray := ⋯ } = #[a].toVector

@[simp]

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

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

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

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

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

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 : α} {l : Vector α n} : a ∈ l ↔ ∃ (m : Nat), ∃ (k : Nat), ∃ (w : m + 1 + k = n), ∃ (s : Vector α m), ∃ (t : Vector α k), l = Vector.cast w (s.push a ++ t)

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

theorem Vector.empty_append {α : Type u_1} {n : Nat} (as : Vector α n) : { toArray := #[], size_toArray := ⋯ } ++ as = Vector.cast ⋯ as

theorem Vector.append_empty {α : Type u_1} {n : Nat} (as : Vector α n) : as ++ { toArray := #[], size_toArray := ⋯ } = as

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

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

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

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

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

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

theorem Vector.getElem_append_left' {α : Type u_1} {m n : Nat} (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < m) : l₁[i] = (l₁ ++ l₂)[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 : Nat} (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < n) : l₂[i] = (l₁ ++ l₂)[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 : α} {l : Vector α n} {l₁ : Vector α m} {l₂ : Vector α k} (w : m + 1 + k = n) (eq : l = Vector.cast w (l₁.push a ++ l₂)) : l[m] = a

@[simp]

theorem Vector.append_singleton {α : Type u_1} {n : Nat} {a : α} {as : Vector α n} : as ++ { toArray := #[a], size_toArray := ⋯ } = as.push a

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

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

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

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

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

theorem Vector.append_eq_append_iff {α : Type u_1} {n m k l : Nat} {a : Vector α n} {b : Vector α m} {c : Vector α k} {d : Vector α l} (w : k + l = n + m) : a ++ b = Vector.cast w (c ++ d) ↔ if h : n ≤ k then ∃ (a' : Vector α (k - n)), c = Vector.cast ⋯ (a ++ a') ∧ b = Vector.cast ⋯ (a' ++ d) else ∃ (c' : Vector α (n - k)), a = Vector.cast ⋯ (c ++ c') ∧ d = Vector.cast ⋯ (c' ++ b)

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Vector.map_eq_append_iff {α : Type u_1} {β : Type u_2} {a✝ a✝¹ : Nat} {l : Vector α (a✝ + a✝¹)} {L₁ : Vector β a✝} {L₂ : Vector β a✝¹} {f : α → β} : map f l = L₁ ++ L₂ ↔ ∃ (l₁ : Vector α a✝), ∃ (l₂ : Vector α a✝¹), l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

theorem Vector.append_eq_map_iff {α : Type u_1} {β : Type u_2} {n✝ : Nat} {L₁ : Vector β n✝} {n✝¹ : Nat} {L₂ : Vector β n✝¹} {l : Vector α (n✝ + n✝¹)} {f : α → β} : L₁ ++ L₂ = map f l ↔ ∃ (l₁ : Vector α n✝), ∃ (l₂ : Vector α n✝¹), l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

flatten

@[simp]

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

@[simp]

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

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

@[simp]

theorem Vector.flatten_singleton {α : Type u_1} {n : Nat} (l : Vector α n) : { toArray := #[l], size_toArray := ⋯ }.flatten = Vector.cast ⋯ l

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

theorem Vector.exists_of_mem_flatten {α✝ : Type u_1} {n✝ n✝¹ : Nat} {L : Vector (Vector α✝ n✝) n✝¹} {a : α✝} : a ∈ L.flatten → ∃ (l : Vector α✝ n✝), l ∈ L ∧ a ∈ l

theorem Vector.mem_flatten_of_mem {α✝ : Type u_1} {n✝ n✝¹ : Nat} {L : Vector (Vector α✝ n✝) n✝¹} {l : Vector α✝ n✝} {a : α✝} (lL : l ∈ L) (al : a ∈ l) : a ∈ L.flatten

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

@[simp]

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

@[simp]

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

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

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

theorem Vector.eq_iff_flatten_eq {α : Type u_1} {n m : Nat} {L L' : Vector (Vector α n) m} : L = L' ↔ L.flatten = L'.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} (l : Vector α n) (f : α → Vector β m) : Array.flatMap (fun (a : α) => (f a).toArray) l.toArray = (l.flatMap f).toArray

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[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 {n m : Nat} {γ : Type u_1} {k : Nat} {α : Type u_2} {β : Type u_3} (l : Vector α n) (f : α → Vector β m) (g : β → Vector γ k) : (l.flatMap f).flatMap g = Vector.cast ⋯ (l.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) (l : Vector α n) : map f (l.flatMap g) = l.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) (l : Vector α n) : (map f l).flatMap g = l.flatMap fun (a : α) => g (f a)

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

mkVector

@[simp]

theorem Vector.mkVector_one {α✝ : Type u_1} {a : α✝} : mkVector 1 a = { toArray := #[a], size_toArray := ⋯ }

theorem Vector.mkVector_succ' {n : Nat} {α✝ : Type u_1} {a : α✝} : mkVector (n + 1) a = Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ mkVector n a)

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

theorem Vector.getElem?_mkVector_of_lt {α✝ : Type u_1} {a : α✝} {n m : Nat} (h : m < n) : (mkVector n a)[m]? = some a

theorem Vector.eq_mkVector_of_mem {α : Type u_1} {n : Nat} {a : α} {l : Vector α n} (h : ∀ (b : α), b ∈ l → b = a) : l = mkVector n a

theorem Vector.eq_mkVector_iff {α : Type u_1} {a : α} {n : Nat} {l : Vector α n} : l = mkVector n a ↔ ∀ (b : α), b ∈ l → b = a

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

@[simp]

theorem Vector.map_const {α : Type u_1} {n : Nat} {β : Type u_2} (l : Vector α n) (b : β) : map (Function.const α b) l = mkVector 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) => mkVector n x

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Vector.append_eq_mkVector_iff {α : Type u_1} {n m : Nat} {l₁ : Vector α n} {l₂ : Vector α m} {a : α} : l₁ ++ l₂ = mkVector (n + m) a ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a

theorem Vector.mkVector_eq_append_iff {α : Type u_1} {n m : Nat} {l₁ : Vector α n} {l₂ : Vector α m} {a : α} : mkVector (n + m) a = l₁ ++ l₂ ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a

@[simp]

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

@[simp]

theorem Vector.flatten_mkVector_empty {n : Nat} {α : Type u_1} : (mkVector n { toArray := #[], size_toArray := ⋯ }).flatten = { toArray := #[], size_toArray := ⋯ }

@[simp]

theorem Vector.flatten_mkVector_singleton {n : Nat} {α✝ : Type u_1} {a : α✝} : (mkVector n { toArray := #[a], size_toArray := ⋯ }).flatten = Vector.cast ⋯ (mkVector n a)

@[simp]

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

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

@[simp]

theorem Vector.sum_mkArray_nat (n a : Nat) : (mkVector n a).sum = n * a

reverse

@[simp]

theorem Vector.reverse_push {α : Type u_1} {n : Nat} (as : Vector α n) (a : α) : (as.push a).reverse = Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ 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} (a : Vector α n) (i : Nat) (hi : i < n) : a.reverse[i] = a[n - 1 - i]

theorem Vector.getElem?_reverse' {α : Type u_1} {n : Nat} {l : Vector α n} (i j : Nat) (h : i + j + 1 = n) : l.reverse[i]? = l[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} {l : Vector α n} {i : Nat} (h : i < n) : l.reverse[i]? = l[n - 1 - i]?

@[simp]

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

theorem Vector.reverse_eq_iff {α : Type u_1} {n : Nat} {as bs : Vector α n} : as.reverse = bs ↔ as = bs.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 ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ ys.reverse)

@[simp]

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

@[simp]

theorem Vector.reverse_append {α : Type u_1} {n m : Nat} (as : Vector α n) (bs : Vector α m) : (as ++ bs).reverse = Vector.cast ⋯ (bs.reverse ++ as.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} (L : Vector (Vector α m) n) : L.flatten.reverse = (map reverse L).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} (L : Vector (Vector α m) n) : L.reverse.flatten = (map reverse L).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 m : Nat} {β : Type u_2} (l : Vector α n) (f : α → Vector β m) : (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f)

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

@[simp]

theorem Vector.reverse_mkVector {α : Type u_1} (n : Nat) (a : α) : (mkVector n a).reverse = mkVector 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 as.size - 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) : { toArray := #[], size_toArray := ⋯ }.extract start stop = Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }

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 : β) (l : Vector α n) (l' : Vector α k) : foldlM f b (l ++ l') = do let b ← foldlM f b l foldlM f b l'

@[simp]

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 { toArray := #[], size_toArray := ⋯ } = pure init

@[simp]

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 { toArray := #[], size_toArray := ⋯ } = 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] (l : Vector α n) (a : α) (f : β → α → m β) (b : β) : foldlM f b (l.push a) = do let b ← foldlM f b l f b a

theorem Vector.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} {n : Nat} (f : β → α → β) (b : β) (l : Vector α n) : foldl f b l = foldlM f b l

theorem Vector.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → β → β) (b : β) (l : Vector α n) : foldr f b l = foldrM f b l

@[simp]

theorem Vector.id_run_foldlM {β : Type u_1} {α : Type u_2} {n : Nat} (f : β → α → Id β) (b : β) (l : Vector α n) : (foldlM f b l).run = foldl f b l

@[simp]

theorem Vector.id_run_foldrM {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → β → Id β) (b : β) (l : Vector α n) : (foldrM f b l).run = foldr f b l

@[simp]

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

@[simp]

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

@[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 : β) (arr : Vector α n) (a : α) : foldrM f init (arr.push a) = do let b ← f a init foldrM f b arr

foldl / foldr

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

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

@[simp]

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

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

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

theorem Vector.foldl_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} (f : α → Option β) (g : γ → β → γ) (l : Vector α n) (init : γ) : Array.foldl g init (Array.filterMap f l.toArray) = foldl (fun (x : γ) (y : α) => match f y with | some b => g x b | none => x) init l

theorem Vector.foldr_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} (f : α → Option β) (g : β → γ → γ) (l : Vector α n) (init : γ) : Array.foldr g init (Array.filterMap f l.toArray) = foldr (fun (x : α) (y : γ) => match f x with | some b => g b y | none => y) init l

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

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

@[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 : β) (l : Vector α n) (l' : Vector α k) : foldrM f b (l ++ l') = do let b ← foldrM f b l' foldrM f b l

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem Vector.foldr_add_const {α : Type u_1} (l : Array α) (a b : Nat) : Array.foldr (fun (x : α) (x : Nat) => x + a) b l = b + a * l.size

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

findRev? and findSomeRev?

@[simp]

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

@[simp]

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

zipWith

@[simp]

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

take

@[simp]

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

swap

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

range

@[simp]

theorem Vector.getElem_range {n : Nat} (i : Nat) (hi : i < n) : (range n)[i] = i

take

@[simp]

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

drop

@[simp]

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

Decidable quantifiers.

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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