mapFinIdx

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

theorem Array.mapFinIdx_induction.go {α : Type u_1} {β : Type u_2} (as : Array α) (f : Fin as.size → α → β) (motive : Nat → Prop) (p : Fin as.size → β → Prop) (hs : ∀ (i : Fin as.size), motive ↑i → p i (f i as[i]) ∧ 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, h⟩ bs[i]) (hm : motive j) : let arr := Array.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, h⟩ arr[i_1]

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

@[simp]

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

@[simp]

theorem Array.size_zipWithIndex {α : Type u_1} (as : Array α) : as.zipWithIndex.size = as.size

@[simp]

theorem Array.getElem_mapFinIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : Fin 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 : Fin 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 : Fin a.size → α → β) : (a.mapFinIdx f).toList = a.toList.mapFinIdx fun (i : Fin a.toList.length) (a_1 : α) => f ⟨↑i, ⋯⟩ a_1

mapIdx

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

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

@[simp]

theorem Array.size_mapIdx {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (as : Array α) : (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 < (Array.mapIdx f as).size) : (Array.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) : (Array.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 α) : (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 : Fin 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 = (List.mapIdx f l).toArray