forall_mem_zipIdx — Mathlib

English

A universal property over l.zipIdx n is equivalent to a pointwise property along l with indices i < length l.

Русский

Универсальность по l.zipIdx n эквивалентна свойству для каждого индекса i < длина l применительно к элементу l[i] и числу n+i.

LaTeX

$$$ (\forall x \in l.zipIdx\ n,\; p\ x) \iff \forall (i : \mathbb{N})\ (\,i < \mathrm{length}\ l),\; p\ (l[i],\; n+i) $$$

Lean4

theorem forall_mem_zipIdx {l : List α} {n : ℕ} {p : α × ℕ → Prop} :
    (∀ x ∈ l.zipIdx n, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], n + i) := by
  simp only [forall_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

Похожие утверждения