### mapFinIdx #

source
theorem Array.mapFinIdx_induction {α : Type u_1} {β : Type u_2} (xs : Array α) (f : (i : Nat) → α → i < xs.size → β) (motive : Nat → Prop) (h0 : motive 0) (p : (i : Nat) → β → i < xs.size → Prop) (hs : ∀ (i : Nat) (h : i < xs.size), motive i → p i (f i xs[i] h) h ∧ motive (i + 1)) :
motive xs.size ∧ ∃ (eq : (xs.mapFinIdx f).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (xs.mapFinIdx f)[i] h
source
theorem Array.mapFinIdx_spec {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {p : (i : Nat) → β → i < xs.size → Prop} (hs : ∀ (i : Nat) (h : i < xs.size), p i (f i xs[i] h) h) :
∃ (eq : (xs.mapFinIdx f).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (xs.mapFinIdx f)[i] h
source
@[simp]
theorem Array.size_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} :
(xs.mapFinIdx f).size = xs.size
source
@[simp]
theorem Array.size_zipIdx {α : Type u_1} {xs : Array α} {k : Nat} :
(xs.zipIdx k).size = xs.size
source
@[simp]
theorem Array.getElem_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {i : Nat} (h : i < (xs.mapFinIdx f).size) :
(xs.mapFinIdx f)[i] = f i xs[i] ⋯
source
@[simp]
theorem Array.getElem?_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {i : Nat} :
(xs.mapFinIdx f)[i]? = xs[i]?.pbind fun (b : α) (h : xs[i]? = some b) => some (f i b ⋯)
source
@[simp]
theorem Array.toList_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} :
(xs.mapFinIdx f).toList = xs.toList.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.toList.length) => f i a h

### mapIdx #

source
theorem Array.mapIdx_induction {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {motive : Nat → Prop} (h0 : motive 0) {p : (i : Nat) → β → i < xs.size → Prop} (hs : ∀ (i : Nat) (h : i < xs.size), motive i → p i (f i xs[i]) h ∧ motive (i + 1)) :
motive xs.size ∧ ∃ (eq : (mapIdx f xs).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (mapIdx f xs)[i] h
source
theorem Array.mapIdx_spec {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {p : (i : Nat) → β → i < xs.size → Prop} (hs : ∀ (i : Nat) (h : i < xs.size), p i (f i xs[i]) h) :
∃ (eq : (mapIdx f xs).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (mapIdx f xs)[i] h
source
@[simp]
theorem Array.size_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} :
(mapIdx f xs).size = xs.size
source
@[simp]
theorem Array.getElem_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {i : Nat} (h : i < (mapIdx f xs).size) :
(mapIdx f xs)[i] = f i xs[i]
source
@[simp]
theorem Array.getElem?_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {i : Nat} :
(mapIdx f xs)[i]? = Option.map (f i) xs[i]?
source
@[simp]
theorem Array.toList_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} :
(mapIdx f xs).toList = List.mapIdx (fun (i : Nat) (a : α) => f i a) xs.toList
source
@[simp]
theorem List.mapFinIdx_toArray {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → α → i < l.length → β} :
l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray
source
@[simp]
theorem List.mapIdx_toArray {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {l : List α} :
Array.mapIdx f l.toArray = (mapIdx f l).toArray

### zipIdx #

source
@[simp]
theorem Array.getElem_zipIdx {α : Type u_1} {xs : Array α} {k i : Nat} (h : i < (xs.zipIdx k).size) :
(xs.zipIdx k)[i] = (xs[i], k + i)
source
@[simp]
theorem Array.zipIdx_toArray {α : Type u_1} {l : List α} {k : Nat} :
l.toArray.zipIdx k = (l.zipIdx k).toArray
source
@[simp]
theorem Array.toList_zipIdx {α : Type u_1} {xs : Array α} {k : Nat} :
(xs.zipIdx k).toList = xs.toList.zipIdx k
source
theorem Array.mk_mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {k i : Nat} {x : α} {xs : Array α} :
(x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = some x
source
theorem Array.mk_mem_zipIdx_iff_getElem? {α : Type u_1} {x : α} {i : Nat} {xs : Array α} :
(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.

source
theorem Array.mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {x : α × Nat} {xs : Array α} {k : Nat} :
x ∈ xs.zipIdx k ↔ k ≤ x.snd ∧ xs[x.snd - k]? = some x.fst
source
theorem Array.mem_zipIdx_iff_getElem? {α : Type u_1} {x : α × Nat} {xs : Array α} :
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.

### mapFinIdx #

source
theorem Array.mapFinIdx_congr {α : Type u_1} {β : Type u_2} {xs ys : Array α} (w : xs = ys) (f : (i : Nat) → α → i < xs.size → β) :
xs.mapFinIdx f = ys.mapFinIdx fun (i : Nat) (a : α) (h : i < ys.size) => f i a ⋯
source
@[simp]
theorem Array.mapFinIdx_empty {α : Type u_1} {β : Type u_2} {f : (i : Nat) → α → i < 0 → β} :
#[].mapFinIdx f = #[]
source
theorem Array.mapFinIdx_eq_ofFn {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} :
xs.mapFinIdx f = ofFn fun (i : Fin xs.size) => f (↑i) xs[i] ⋯
source
theorem Array.mapFinIdx_append {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : (i : Nat) → α → i < (xs ++ ys).size → β} :
(xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.size) => f i a ⋯) ++ ys.mapFinIdx fun (i : Nat) (a : α) (h : i < ys.size) => f (i + xs.size) a ⋯
source
@[simp]
theorem Array.mapFinIdx_push {α : Type u_1} {β : Type u_2} {xs : Array α} {a : α} {f : (i : Nat) → α → i < (xs.push a).size → β} :
(xs.push a).mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a_1 : α) (h : i < xs.size) => f i a_1 ⋯).push (f xs.size a ⋯)
source
theorem Array.mapFinIdx_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : (i : Nat) → α → i < 1 → β} :
#[a].mapFinIdx f = #[f 0 a mapFinIdx_singleton._proof_1]
source
theorem Array.mapFinIdx_eq_zipIdx_map {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} :
xs.mapFinIdx f = map (fun (x : { x : α × Nat // x ∈ xs.zipIdx }) => match x with | ⟨(x, i), m⟩ => f i x ⋯) xs.zipIdx.attach
source
@[simp]
theorem Array.mapFinIdx_eq_empty_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} :
xs.mapFinIdx f = #[] ↔ xs = #[]
source
theorem Array.mapFinIdx_ne_empty_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} :
xs.mapFinIdx f ≠ #[] ↔ xs ≠ #[]
source
theorem Array.exists_of_mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} (h : b ∈ xs.mapFinIdx f) :
∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] h = b
source
@[simp]
theorem Array.mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} :
b ∈ xs.mapFinIdx f ↔ ∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] h = b
source
theorem Array.mapFinIdx_eq_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {ys : Array β} :
xs.mapFinIdx f = ys ↔ ∃ (h : ys.size = xs.size), ∀ (i : Nat) (h_1 : i < xs.size), ys[i] = f i xs[i] h_1
source
@[simp]
theorem Array.mapFinIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {b : β} :
xs.mapFinIdx f = #[b] ↔ ∃ (a : α), ∃ (w : xs = #[a]), f 0 a ⋯ = b
source
theorem Array.mapFinIdx_eq_append_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {ys zs : Array β} :
xs.mapFinIdx f = ys ++ zs ↔ ∃ (ys' : Array α), ∃ (zs' : Array α), ∃ (w : xs = ys' ++ zs'), (ys'.mapFinIdx fun (i : Nat) (a : α) (h : i < ys'.size) => f i a ⋯) = ys ∧ (zs'.mapFinIdx fun (i : Nat) (a : α) (h : i < zs'.size) => f (i + ys'.size) a ⋯) = zs
source
theorem Array.mapFinIdx_eq_push_iff {α : Type u_1} {β : Type u_2} {ys : Array β} {xs : Array α} {b : β} {f : (i : Nat) → α → i < xs.size → β} :
xs.mapFinIdx f = ys.push b ↔ ∃ (zs : Array α), ∃ (a : α), ∃ (w : xs = zs.push a), (zs.mapFinIdx fun (i : Nat) (a_1 : α) (h : i < zs.size) => f i a_1 ⋯) = ys ∧ b = f (xs.size - 1) a ⋯
source
theorem Array.mapFinIdx_eq_mapFinIdx_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : (i : Nat) → α → i < xs.size → β} :
xs.mapFinIdx f = xs.mapFinIdx g ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = g i xs[i] h
source
@[simp]
theorem Array.mapFinIdx_mapFinIdx {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {g : (i : Nat) → β → i < (xs.mapFinIdx f).size → γ} :
(xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.size) => g i (f i a h) ⋯
source
theorem Array.mapFinIdx_eq_replicate_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {b : β} :
xs.mapFinIdx f = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b
source
@[reducible, inline, deprecated Array.mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
abbrev Array.mapFinIdx_eq_mkArray_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {b : β} :
xs.mapFinIdx f = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b
Equations

- @Array.mapFinIdx_eq_mkArray_iff = @Array.mapFinIdx_eq_replicate_iff

Instances For

source
@[simp]
theorem Array.mapFinIdx_reverse {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.reverse.size → β} :
xs.reverse.mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.size) => f (xs.size - 1 - i) a ⋯).reverse

### mapIdx #

source
@[simp]
theorem Array.mapIdx_empty {α : Type u_1} {β : Type u_2} {f : Nat → α → β} :
mapIdx f #[] = #[]
source
@[simp]
theorem Array.mapFinIdx_eq_mapIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {g : Nat → α → β} (h : ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = g i xs[i]) :
xs.mapFinIdx f = mapIdx g xs
source
theorem Array.mapIdx_eq_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} :
mapIdx f xs = xs.mapFinIdx fun (i : Nat) (a : α) (x : i < xs.size) => f i a
source
theorem Array.mapIdx_eq_zipIdx_map {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} :
mapIdx f xs = map (fun (x : α × Nat) => match x with | (a, i) => f i a) xs.zipIdx
source
theorem Array.mapIdx_append {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs ys : Array α} :
mapIdx f (xs ++ ys) = mapIdx f xs ++ mapIdx (fun (i : Nat) => f (i + xs.size)) ys
source
@[simp]
theorem Array.mapIdx_push {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} {a : α} :
mapIdx f (xs.push a) = (mapIdx f xs).push (f xs.size a)
source
theorem Array.mapIdx_singleton {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {a : α} :
mapIdx f #[a] = #[f 0 a]
source
@[simp]
theorem Array.mapIdx_eq_empty_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} :
mapIdx f xs = #[] ↔ xs = #[]
source
theorem Array.mapIdx_ne_empty_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} :
mapIdx f xs ≠ #[] ↔ xs ≠ #[]
source
theorem Array.exists_of_mem_mapIdx {β : Type u_1} {α : Type u_2} {f : Nat → α → β} {b : β} {xs : Array α} (h : b ∈ mapIdx f xs) :
∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] = b
source
@[simp]
theorem Array.mem_mapIdx {β : Type u_1} {α : Type u_2} {f : Nat → α → β} {b : β} {xs : Array α} :
b ∈ mapIdx f xs ↔ ∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] = b
source
theorem Array.mapIdx_eq_push_iff {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {ys : Array β} {xs : Array α} {b : β} :
mapIdx f xs = ys.push b ↔ ∃ (a : α), ∃ (zs : Array α), xs = zs.push a ∧ mapIdx f zs = ys ∧ f zs.size a = b
source
@[simp]
theorem Array.mapIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {b : β} :
mapIdx f xs = #[b] ↔ ∃ (a : α), xs = #[a] ∧ f 0 a = b
source
theorem Array.mapIdx_eq_append_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {ys zs : Array β} :
mapIdx f xs = ys ++ zs ↔ ∃ (xs' : Array α), ∃ (zs' : Array α), xs = xs' ++ zs' ∧ mapIdx f xs' = ys ∧ mapIdx (fun (i : Nat) => f (i + xs'.size)) zs' = zs
source
theorem Array.mapIdx_eq_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {ys : Array α✝} {xs : Array α} :
mapIdx f xs = ys ↔ ∀ (i : Nat), ys[i]? = Option.map (f i) xs[i]?
source
theorem Array.mapIdx_eq_mapIdx_iff {α : Type u_1} {α✝ : Type u_2} {f g : Nat → α → α✝} {xs : Array α} :
mapIdx f xs = mapIdx g xs ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = g i xs[i]
source
@[simp]
theorem Array.mapIdx_set {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} :
mapIdx f (xs.set i a h) = (mapIdx f xs).set i (f i a) ⋯
source
@[simp]
theorem Array.mapIdx_setIfInBounds {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} {i : Nat} {a : α} :
mapIdx f (xs.setIfInBounds i a) = (mapIdx f xs).setIfInBounds i (f i a)
source
@[simp]
theorem Array.back?_mapIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} :
(mapIdx f xs).back? = Option.map (f (xs.size - 1)) xs.back?
source
@[simp]
theorem Array.back_mapIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} (h : 0 < (mapIdx f xs).size) :
(mapIdx f xs).back h = f (xs.size - 1) (xs.back ⋯)
source
@[simp]
theorem Array.mapIdx_mapIdx {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : Nat → α → β} {g : Nat → β → γ} :
mapIdx g (mapIdx f xs) = mapIdx (fun (i : Nat) => g i ∘ f i) xs
source
theorem Array.mapIdx_eq_replicate_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {b : β} :
mapIdx f xs = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b
source
@[reducible, inline, deprecated Array.mapIdx_eq_replicate_iff (since := "2025-03-18")]
abbrev Array.mapIdx_eq_mkArray_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {b : β} :
mapIdx f xs = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b
Equations

- @Array.mapIdx_eq_mkArray_iff = @Array.mapIdx_eq_replicate_iff

Instances For

source
@[simp]
theorem Array.mapIdx_reverse {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} :
mapIdx f xs.reverse = (mapIdx (fun (i : Nat) => f (xs.size - 1 - i)) xs).reverse
source
theorem List.mapFinIdxM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : (i : Nat) → α → i < l.length → m β} :
l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f
source
theorem List.mapIdxM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : Nat → α → m β} :
Array.mapIdxM f l.toArray = toArray <$> mapIdxM f l
source
theorem Array.toList_mapFinIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : (i : Nat) → α → i < xs.size → m β} :
toList <$> xs.mapFinIdxM f = xs.toList.mapFinIdxM f
source
theorem Array.toList_mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : Nat → α → m β} :
toList <$> mapIdxM f xs = List.mapIdxM f xs.toList