mapFinIdx

@[simp]

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

@[simp]

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

mapIdx

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

zipIdx

@[simp]

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

@[simp]

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

@[simp]

theorem Vector.zipIdx_toVector {α : Type u_1} {l : Array α} {k : Nat} : l.toVector.zipIdx k = Vector.cast ⋯ (l.zipIdx k).toVector

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

theorem Vector.mk_mem_zipIdx_iff_getElem? {α : Type u_1} {n : Nat} {x : α} {i : Nat} {l : Vector α n} : (x, i) ∈ l.zipIdx ↔ l[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} {l : Vector α n} {k : Nat} : x ∈ l.zipIdx k ↔ k ≤ x.snd ∧ l[x.snd - k]? = some x.fst

theorem Vector.mem_zipIdx_iff_getElem? {α : Type u_1} {n : Nat} {x : α × Nat} {l : Vector α n} : x ∈ l.zipIdx ↔ l[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} (a : Vector α n) (k : Nat := 0) : (a.zipIdx k).toList = a.toList.zipIdx k

Equations

• @Vector.toList_zipWithIndex = @Vector.toList_zipIdx

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

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

Equations

• @Vector.getElem_zipWithIndex = @Vector.getElem_zipIdx

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

abbrev Vector.zipWithIndex_toVector {α : Type u_1} {l : Array α} {k : Nat} : l.toVector.zipIdx k = Vector.cast ⋯ (l.zipIdx k).toVector

Equations

• @Vector.zipWithIndex_toVector = @Vector.zipIdx_toVector

@[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} {l : Vector α n} {k : Nat} : (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Equations

• @Vector.mk_mem_zipWithIndex_iff_le_and_getElem?_sub = @Vector.mk_mem_zipIdx_iff_le_and_getElem?_sub

@[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} {l : Vector α n} : (x, i) ∈ l.zipIdx ↔ l[i]? = some x

Equations

• @Vector.mk_mem_zipWithIndex_iff_getElem? = @Vector.mk_mem_zipIdx_iff_getElem?

@[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} {l : Vector α n} {k : Nat} : x ∈ l.zipIdx k ↔ k ≤ x.snd ∧ l[x.snd - k]? = some x.fst

Equations

• @Vector.mem_zipWithIndex_iff_le_and_getElem?_sub = @Vector.mem_zipIdx_iff_le_and_getElem?_sub

@[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} {l : Vector α n} : x ∈ l.zipIdx ↔ l[x.snd]? = some x.fst

Equations

• @Vector.mem_zipWithIndex_iff_getElem? = @Vector.mem_zipIdx_iff_getElem?

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} {K : Vector α n} {L : Vector α m} {f : (i : Nat) → α → i < n + m → β} : (K ++ L).mapFinIdx f = (K.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => f i a ⋯) ++ L.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} {l : Vector α n} {a : α} {f : (i : Nat) → α → i < n + 1 → β} : (l.push a).mapFinIdx f = (l.mapFinIdx fun (i : Nat) (a : α) (h : i < n) => f i a ⋯).push (f l.size 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.exists_of_mem_mapFinIdx {β : Type u_1} {α : Type u_2} {n : Nat} {b : β} {l : Vector α n} {f : (i : Nat) → α → i < n → β} (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat), ∃ (h : i < n), f i l[i] h = b

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

theorem Vector.mapFinIdx_reverse {α : Type u_1} {n : Nat} {β : Type u_2} {l : Vector α n} {f : (i : Nat) → α → i < n → β} : l.reverse.mapFinIdx f = (l.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} {l : Vector α n} {f : (i : Nat) → α → i < n → β} {g : Nat → α → β} (h : ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i]) : l.mapFinIdx f = mapIdx g l

theorem Vector.mapIdx_eq_mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} {l : Vector α n} {f : Nat → α → β} : mapIdx f l = l.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} {l : Vector α n} {f : Nat → α → β} : mapIdx f l = map (fun (x : α × Nat) => match x with | (a, i) => f i a) l.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} {l : Vector α n} {f : Nat → α → β} : mapIdx f l = map (fun (x : α × Nat) => match x with | (a, i) => f i a) l.zipIdx

Equations

• @Vector.mapIdx_eq_zipWithIndex_map = @Vector.mapIdx_eq_zipIdx_map

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

@[simp]

theorem Vector.mapIdx_push {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : Nat → α → α✝} {l : Vector α n} {a : α} : mapIdx f (l.push a) = (mapIdx f l).push (f l.size 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 : β} {l : Vector α n} (h : b ∈ mapIdx f l) : ∃ (i : Nat), ∃ (h : i < n), f i l[i] = b

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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