exists_mem_zipIdx — Mathlib

English

Variant with zipIdx specialized to 0: there exists i < length l such that p(l[i], i) holds.

Русский

Вариант со специализацией zipIdx к 0: существует i < длина l такое, что p(l[i], i) выполняется.

LaTeX

$$$ (\exists x \in l.zipIdx,\; p\ x) \iff \exists i (\,i < \mathrm{length}\ l),\; p (l[i], i) $$$

Lean4

theorem exists_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 [exists_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

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