mapFinIdx

@[simp]

theorem Vector.getElem_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} {i : Nat} (h : i < n) : (xs.mapFinIdx f)[i] = f i xs[i] h

@[simp]

theorem Vector.getElem?_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} {i : Nat} : (xs.mapFinIdx f)[i]? = xs[i]?.pbind fun (b : α) (h : xs[i]? = some b) => some (f i b ⋯)

mapIdx

@[simp]

theorem Vector.getElem_mapIdx {α : Type u_1} {β : Type u_2} {n : Nat} {f : Nat → α → β} {xs : Vector α n} {i : Nat} (h : i < n) : (mapIdx f xs)[i] = f i xs[i]

@[simp]

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

@[simp]

theorem Array.mapFinIdx_toVector {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : xs.toVector.mapFinIdx f = Vector.cast ⋯ (xs.mapFinIdx f).toVector

@[simp]

theorem Array.mapIdx_toVector {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} : Vector.mapIdx f xs.toVector = Vector.cast ⋯ (mapIdx f xs).toVector

zipIdx

@[simp]

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

@[simp]

theorem Vector.getElem_zipIdx {α : Type u_1} {n k : Nat} {xs : Vector α n} {i : Nat} {h : i < n} : (xs.zipIdx k)[i] = (xs[i], k + i)

theorem Vector.mk_mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {n : Nat} {x : α} {i : Nat} {xs : Vector α n} {k : Nat} : (x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = some x

theorem Vector.mk_mem_zipIdx_iff_getElem? {α : Type u_1} {n : Nat} {x : α} {i : Nat} {xs : Vector α n} : (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x

Variant of mk_mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

theorem Vector.mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {n : Nat} {x : α × Nat} {xs : Vector α n} {k : Nat} : x ∈ xs.zipIdx k ↔ k ≤ x.snd ∧ xs[x.snd - k]? = some x.fst

theorem Vector.mem_zipIdx_iff_getElem? {α : Type u_1} {n : Nat} {x : α × Nat} {xs : Vector α n} : x ∈ xs.zipIdx ↔ xs[x.snd]? = some x.fst

Variant of mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

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

abbrev Vector.toList_zipWithIndex {α : Type u_1} {n : Nat} {xs : Vector α n} (k : Nat := 0) : (xs.zipIdx k).toList = xs.toList.zipIdx k

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

abbrev Vector.getElem_zipWithIndex {α : Type u_1} {n k : Nat} {xs : Vector α n} {i : Nat} {h : i < n} : (xs.zipIdx k)[i] = (xs[i], k + i)

@[reducible, inline, deprecated Vector.mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-27")]

abbrev Vector.mk_mem_zipWithIndex_iff_le_and_getElem?_sub {α : Type u_1} {n : Nat} {x : α} {i : Nat} {xs : Vector α n} {k : Nat} : (x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = some x

@[reducible, inline, deprecated Vector.mk_mem_zipIdx_iff_getElem? (since := "2025-01-27")]

abbrev Vector.mk_mem_zipWithIndex_iff_getElem? {α : Type u_1} {n : Nat} {x : α} {i : Nat} {xs : Vector α n} : (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x

@[reducible, inline, deprecated Vector.mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-27")]

abbrev Vector.mem_zipWithIndex_iff_le_and_getElem?_sub {α : Type u_1} {n : Nat} {x : α × Nat} {xs : Vector α n} {k : Nat} : x ∈ xs.zipIdx k ↔ k ≤ x.snd ∧ xs[x.snd - k]? = some x.fst

@[reducible, inline, deprecated Vector.mem_zipIdx_iff_getElem? (since := "2025-01-27")]

abbrev Vector.mem_zipWithIndex_iff_getElem? {α : Type u_1} {n : Nat} {x : α × Nat} {xs : Vector α n} : x ∈ xs.zipIdx ↔ xs[x.snd]? = some x.fst

mapFinIdx

theorem Vector.mapFinIdx_congr {α : Type u_1} {n : Nat} {β : Type u_2} {xs ys : Vector α n} (w : xs = ys) (f : (i : Nat) → α → i < n → β) : xs.mapFinIdx f = ys.mapFinIdx f

@[simp]

theorem Vector.mapFinIdx_empty {α : Type u_1} {β : Type u_2} {f : (i : Nat) → α → i < 0 → β} : { toArray := #[], size_toArray := ⋯ }.mapFinIdx f = { toArray := #[], size_toArray := ⋯ }

theorem Vector.mapFinIdx_eq_ofFn {α : Type u_1} {n : Nat} {β : Type u_2} {as : Vector α n} {f : (i : Nat) → α → i < n → β} : as.mapFinIdx f = ofFn fun (i : Fin n) => f (↑i) as[i] ⋯

theorem Vector.mapFinIdx_append {α : Type u_1} {n m : Nat} {β : Type u_2} {xs : Vector α n} {ys : Vector α m} {f : (i : Nat) → α → i < n + m → β} : (xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => f i a ⋯) ++ ys.mapFinIdx fun (i : Nat) (a : α) (h : i < m) => f (i + n) a ⋯

@[simp]

theorem Vector.mapFinIdx_push {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {a : α} {f : (i : Nat) → α → i < n + 1 → β} : (xs.push a).mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => f i a ⋯).push (f n a ⋯)

theorem Vector.mapFinIdx_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : (i : Nat) → α → i < 1 → β} : { toArray := #[a], size_toArray := ⋯ }.mapFinIdx f = { toArray := #[f 0 a ⋯], size_toArray := ⋯ }

theorem Vector.mapFinIdx_eq_zipIdx_map {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} : xs.mapFinIdx f = map (fun (x : { x : α × Nat // x ∈ xs.zipIdx }) => match x with | ⟨(x, i), m⟩ => f i x ⋯) xs.zipIdx.attach

theorem Vector.exists_of_mem_mapFinIdx {β : Type u_1} {α : Type u_2} {n : Nat} {b : β} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} (h : b ∈ xs.mapFinIdx f) : ∃ (i : Nat), ∃ (h : i < n), f i xs[i] h = b

@[simp]

theorem Vector.mem_mapFinIdx {β : Type u_1} {α : Type u_2} {n : Nat} {b : β} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} : b ∈ xs.mapFinIdx f ↔ ∃ (i : Nat), ∃ (h : i < n), f i xs[i] h = b

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

@[simp]

theorem Vector.mapFinIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {xs : Vector α 1} {f : (i : Nat) → α → i < 1 → β} {b : β} : xs.mapFinIdx f = { toArray := #[b], size_toArray := ⋯ } ↔ ∃ (a : α), xs = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a ⋯ = b

theorem Vector.mapFinIdx_eq_append_iff {α : Type u_1} {n m : Nat} {β : Type u_2} {xs : Vector α (n + m)} {f : (i : Nat) → α → i < n + m → β} {ys : Vector β n} {zs : Vector β m} : xs.mapFinIdx f = ys ++ zs ↔ ∃ (ys' : Vector α n), ∃ (zs' : Vector α m), xs = ys' ++ zs' ∧ (ys'.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => f i a ⋯) = ys ∧ (zs'.mapFinIdx fun (i : Nat) (a : α) (h : i < m) => f (i + n) a ⋯) = zs

theorem Vector.mapFinIdx_eq_push_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α (n + 1)} {b : β} {f : (i : Nat) → α → i < n + 1 → β} {ys : Vector β n} : xs.mapFinIdx f = ys.push b ↔ ∃ (zs : Vector α n), ∃ (a : α), xs = zs.push a ∧ (zs.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => f i a ⋯) = ys ∧ b = f n a ⋯

theorem Vector.mapFinIdx_eq_mapFinIdx_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f g : (i : Nat) → α → i < n → β} : xs.mapFinIdx f = xs.mapFinIdx g ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = g i xs[i] h

@[simp]

theorem Vector.mapFinIdx_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} {g : (i : Nat) → β → i < n → γ} : (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => g i (f i a h) h

theorem Vector.mapFinIdx_eq_replicate_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} {b : β} : xs.mapFinIdx f = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = b

@[reducible, inline, deprecated Vector.mapFinIdx_eq_replicate_iff (since := "2025-03-18")]

abbrev Vector.mapFinIdx_eq_mkVector_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} {b : β} : xs.mapFinIdx f = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = b

@[simp]

theorem Vector.mapFinIdx_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} : xs.reverse.mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => f (n - 1 - i) a ⋯).reverse

mapIdx

@[simp]

theorem Vector.mapIdx_empty {α : Type u_1} {β : Type u_2} {f : Nat → α → β} : mapIdx f { toArray := #[], size_toArray := ⋯ } = { toArray := #[], size_toArray := ⋯ }

@[simp]

theorem Vector.mapFinIdx_eq_mapIdx {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : (i : Nat) → α → i < n → β} {g : Nat → α → β} (h : ∀ (i : Nat) (h : i < n), f i xs[i] h = g i xs[i]) : xs.mapFinIdx f = mapIdx g xs

theorem Vector.mapIdx_eq_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : Nat → α → β} : mapIdx f xs = xs.mapFinIdx fun (i : Nat) (a : α) (x : i < n) => f i a

theorem Vector.mapIdx_eq_zipIdx_map {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : Nat → α → β} : mapIdx f xs = map (fun (x : α × Nat) => match x with | (a, i) => f i a) xs.zipIdx

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

abbrev Vector.mapIdx_eq_zipWithIndex_map {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : Nat → α → β} : mapIdx f xs = map (fun (x : α × Nat) => match x with | (a, i) => f i a) xs.zipIdx

theorem Vector.mapIdx_append {α : Type u_1} {n m : Nat} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Vector α n} {ys : Vector α m} : mapIdx f (xs ++ ys) = mapIdx f xs ++ mapIdx (fun (i : Nat) => f (i + n)) ys

@[simp]

theorem Vector.mapIdx_push {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Vector α n} {a : α} : mapIdx f (xs.push a) = (mapIdx f xs).push (f n a)

theorem Vector.mapIdx_singleton {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {a : α} : mapIdx f { toArray := #[a], size_toArray := ⋯ } = { toArray := #[f 0 a], size_toArray := ⋯ }

theorem Vector.exists_of_mem_mapIdx {β : Type u_1} {α : Type u_2} {n : Nat} {f : Nat → α → β} {b : β} {xs : Vector α n} (h : b ∈ mapIdx f xs) : ∃ (i : Nat), ∃ (h : i < n), f i xs[i] = b

@[simp]

theorem Vector.mem_mapIdx {β : Type u_1} {α : Type u_2} {n : Nat} {f : Nat → α → β} {b : β} {xs : Vector α n} : b ∈ mapIdx f xs ↔ ∃ (i : Nat), ∃ (h : i < n), f i xs[i] = b

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

theorem Vector.mapIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {xs : Vector α 1} {f : Nat → α → β} {b : β} : mapIdx f xs = { toArray := #[b], size_toArray := ⋯ } ↔ ∃ (a : α), xs = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a = b

theorem Vector.mapIdx_eq_append_iff {α : Type u_1} {n m : Nat} {β : Type u_2} {xs : Vector α (n + m)} {f : Nat → α → β} {ys : Vector β n} {zs : Vector β m} : mapIdx f xs = ys ++ zs ↔ ∃ (ys' : Vector α n), ∃ (zs' : Vector α m), xs = ys' ++ zs' ∧ mapIdx f ys' = ys ∧ mapIdx (fun (i : Nat) => f (i + n)) zs' = zs

theorem Vector.mapIdx_eq_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : Nat → α → β} {ys : Vector β n} : mapIdx f xs = ys ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = ys[i]

theorem Vector.mapIdx_eq_mapIdx_iff {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f g : Nat → α → α✝} {xs : Vector α n} : mapIdx f xs = mapIdx g xs ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = g i xs[i]

@[simp]

theorem Vector.mapIdx_set {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Vector α n} {i : Nat} {h : i < n} {a : α} : mapIdx f (xs.set i a h) = (mapIdx f xs).set i (f i a) h

@[simp]

theorem Vector.mapIdx_setIfInBounds {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Vector α n} {i : Nat} {a : α} : mapIdx f (xs.setIfInBounds i a) = (mapIdx f xs).setIfInBounds i (f i a)

@[simp]

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

@[simp]

theorem Vector.back_mapIdx {n : Nat} {α : Type u_1} {β : Type u_2} [NeZero n] {xs : Vector α n} {f : Nat → α → β} : (mapIdx f xs).back = f (n - 1) xs.back

@[simp]

theorem Vector.mapIdx_mapIdx {α : Type u_1} {n : Nat} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : Nat → α → β} {g : Nat → β → γ} : mapIdx g (mapIdx f xs) = mapIdx (fun (i : Nat) => g i ∘ f i) xs

theorem Vector.mapIdx_eq_replicate_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : Nat → α → β} {b : β} : mapIdx f xs = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = b

@[reducible, inline, deprecated Vector.mapIdx_eq_replicate_iff (since := "2025-03-18")]

abbrev Vector.mapIdx_eq_mkVector_iff {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : Nat → α → β} {b : β} : mapIdx f xs = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = b

@[simp]

theorem Vector.mapIdx_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : Nat → α → β} : mapIdx f xs.reverse = (mapIdx (fun (i : Nat) => f (n - 1 - i)) xs).reverse

theorem Vector.toArray_mapFinIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} {f : (i : Nat) → α → i < n → m β} : toArray <$> xs.mapFinIdxM f = xs.toArray.mapFinIdxM fun (i : Nat) (x : α) (h : i < xs.toArray.size) => f i x ⋯

theorem Vector.toArray_mapFinIdxM.go {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} {f : (i : Nat) → α → i < n → m β} (i j : Nat) (inv : i + j = n) (bs : Vector β (n - i)) : toArray <$> mapFinIdxM.map xs f i j inv bs = Array.mapFinIdxM.map xs.toArray (fun (i : Nat) (x : α) (h : i < xs.toArray.size) => f i x ⋯) i j ⋯ bs.toArray

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