mapFinIdx

theorem Array.mapFinIdx_induction {α : Type u_1} {β : Type u_2} (as : Array α) (f : (i : Nat) → α → i < as.size → β) (motive : Nat → Prop) (h0 : motive 0) (p : (i : Nat) → β → i < as.size → Prop) (hs : ∀ (i : Nat) (h : i < as.size), motive i → p i (f i as[i] h) h ∧ motive (i + 1)) : motive as.size ∧ ∃ (eq : (as.mapFinIdx f).size = as.size), ∀ (i : Nat) (h : i < as.size), p i (as.mapFinIdx f)[i] h

theorem Array.mapFinIdx_induction.go {α : Type u_1} {β : Type u_2} (as : Array α) (f : (i : Nat) → α → i < as.size → β) (motive : Nat → Prop) (p : (i : Nat) → β → i < as.size → Prop) (hs : ∀ (i : Nat) (h : i < as.size), motive i → p i (f i as[i] h) h ∧ motive (i + 1)) {bs : Array β} {i j : Nat} {h : i + j = as.size} (h₁ : j = bs.size) (h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) (hm : motive j) : let arr := mapFinIdxM.map as f i j h bs; motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i_1 : Nat) (h : i_1 < as.size), p i_1 arr[i_1] h

theorem Array.mapFinIdx_spec {α : Type u_1} {β : Type u_2} (as : Array α) (f : (i : Nat) → α → i < as.size → β) (p : (i : Nat) → β → i < as.size → Prop) (hs : ∀ (i : Nat) (h : i < as.size), p i (f i as[i] h) h) : ∃ (eq : (as.mapFinIdx f).size = as.size), ∀ (i : Nat) (h : i < as.size), p i (as.mapFinIdx f)[i] h

@[simp]

theorem Array.size_mapFinIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : (i : Nat) → α → i < a.size → β) : (a.mapFinIdx f).size = a.size

@[simp]

theorem Array.size_zipIdx {α : Type u_1} (as : Array α) (k : Nat) : (as.zipIdx k).size = as.size

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

abbrev Array.size_zipWithIndex {α : Type u_1} (as : Array α) (k : Nat) : (as.zipIdx k).size = as.size

Equations

• @Array.size_zipWithIndex = @Array.size_zipIdx

@[simp]

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

@[simp]

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

@[simp]

theorem Array.toList_mapFinIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : (i : Nat) → α → i < a.size → β) : (a.mapFinIdx f).toList = a.toList.mapFinIdx fun (i : Nat) (a_1 : α) (h : i < a.toList.length) => f i a_1 h

mapIdx

theorem Array.mapIdx_induction {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (as : Array α) (motive : Nat → Prop) (h0 : motive 0) (p : (i : Nat) → β → i < as.size → Prop) (hs : ∀ (i : Nat) (h : i < as.size), motive i → p i (f i as[i]) h ∧ motive (i + 1)) : motive as.size ∧ ∃ (eq : (mapIdx f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p i (mapIdx f as)[i] h

theorem Array.mapIdx_spec {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (as : Array α) (p : (i : Nat) → β → i < as.size → Prop) (hs : ∀ (i : Nat) (h : i < as.size), p i (f i as[i]) h) : ∃ (eq : (mapIdx f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p i (mapIdx f as)[i] h

@[simp]

theorem Array.size_mapIdx {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (as : Array α) : (mapIdx f as).size = as.size

@[simp]

theorem Array.getElem_mapIdx {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (as : Array α) (i : Nat) (h : i < (mapIdx f as).size) : (mapIdx f as)[i] = f i as[i]

@[simp]

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

@[simp]

theorem Array.toList_mapIdx {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (as : Array α) : (mapIdx f as).toList = List.mapIdx (fun (i : Nat) (a : α) => f i a) as.toList

@[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

@[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

@[simp]

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

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

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

Equations

• @Array.getElem_zipWithIndex = @Array.getElem_zipIdx

@[simp]

theorem Array.zipIdx_toArray {α : Type u_1} {l : List α} {k : Nat} : l.toArray.zipIdx k = (l.zipIdx k).toArray

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

abbrev Array.zipWithIndex_toArray {α : Type u_1} {l : List α} {k : Nat} : l.toArray.zipIdx k = (l.zipIdx k).toArray

Equations

• @Array.zipWithIndex_toArray = @Array.zipIdx_toArray

@[simp]

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

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

abbrev Array.toList_zipWithIndex {α : Type u_1} (a : Array α) (k : Nat) : (a.zipIdx k).toList = a.toList.zipIdx k

Equations

• @Array.toList_zipWithIndex = @Array.toList_zipIdx

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

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

theorem Array.mem_zipIdx_iff_getElem? {α : Type u_1} {x : α × Nat} {l : Array α} : 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 Array.mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]

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

Equations

• @Array.mk_mem_zipWithIndex_iff_getElem? = @Array.mk_mem_zipIdx_iff_getElem?

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

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

Equations

• @Array.mem_zipWithIndex_iff_getElem? = @Array.mem_zipIdx_iff_getElem?

mapFinIdx

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 ⋯

@[simp]

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

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

theorem Array.mapFinIdx_append {α : Type u_1} {β : Type u_2} {K L : Array α} {f : (i : Nat) → α → i < (K ++ L).size → β} : (K ++ L).mapFinIdx f = (K.mapFinIdx fun (i : Nat) (a : α) (h : i < K.size) => f i a ⋯) ++ L.mapFinIdx fun (i : Nat) (a : α) (h : i < L.size) => f (i + K.size) a ⋯

@[simp]

theorem Array.mapFinIdx_push {α : Type u_1} {β : Type u_2} {l : Array α} {a : α} {f : (i : Nat) → α → i < (l.push a).size → β} : (l.push a).mapFinIdx f = (l.mapFinIdx fun (i : Nat) (a_1 : α) (h : i < l.size) => f i a_1 ⋯).push (f l.size a ⋯)

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

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

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

abbrev Array.mapFinIdx_eq_zipWithIndex_map {α : Type u_1} {β : Type u_2} {l : Array α} {f : (i : Nat) → α → i < l.size → β} : l.mapFinIdx f = map (fun (x : { x : α × Nat // x ∈ l.zipIdx }) => match x with | ⟨(x, i), m⟩ => f i x ⋯) l.zipIdx.attach

Equations

• @Array.mapFinIdx_eq_zipWithIndex_map = @Array.mapFinIdx_eq_zipIdx_map

@[simp]

theorem Array.mapFinIdx_eq_empty_iff {α : Type u_1} {β : Type u_2} {l : Array α} {f : (i : Nat) → α → i < l.size → β} : l.mapFinIdx f = #[] ↔ l = #[]

theorem Array.mapFinIdx_ne_empty_iff {α : Type u_1} {β : Type u_2} {l : Array α} {f : (i : Nat) → α → i < l.size → β} : l.mapFinIdx f ≠ #[] ↔ l ≠ #[]

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

@[simp]

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

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

@[simp]

theorem Array.mapFinIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {l : Array α} {f : (i : Nat) → α → i < l.size → β} {b : β} : l.mapFinIdx f = #[b] ↔ ∃ (a : α), ∃ (w : l = #[a]), f 0 a ⋯ = b

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

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

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

@[simp]

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

theorem Array.mapFinIdx_eq_mkArray_iff {α : Type u_1} {β : Type u_2} {l : Array α} {f : (i : Nat) → α → i < l.size → β} {b : β} : l.mapFinIdx f = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] h = b

@[simp]

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

mapIdx

@[simp]

theorem Array.mapIdx_empty {α : Type u_1} {β : Type u_2} {f : Nat → α → β} : mapIdx f #[] = #[]

@[simp]

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

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

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

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

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

Equations

• @Array.mapIdx_eq_zipWithIndex_map = @Array.mapIdx_eq_zipIdx_map

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

@[simp]

theorem Array.mapIdx_push {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {l : Array α} {a : α} : mapIdx f (l.push a) = (mapIdx f l).push (f l.size a)

theorem Array.mapIdx_singleton {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {a : α} : mapIdx f #[a] = #[f 0 a]

@[simp]

theorem Array.mapIdx_eq_empty_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {l : Array α} : mapIdx f l = #[] ↔ l = #[]

theorem Array.mapIdx_ne_empty_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {l : Array α} : mapIdx f l ≠ #[] ↔ l ≠ #[]

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

@[simp]

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

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

@[simp]

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

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

theorem Array.mapIdx_eq_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {l' : Array α✝} {l : Array α} : mapIdx f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Array.mapIdx_eq_mkArray_iff {α : Type u_1} {β : Type u_2} {l : Array α} {f : Nat → α → β} {b : β} : mapIdx f l = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] = b

@[simp]

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