forall_mem_zipIdx' — Mathlib

English

There exists an element in l.zipIdx n that satisfies p, equivalently there exists an index i < length l with p(l[i], n+i).

Русский

Существует элемент в l.zipIdx n, удовлетворяющий p, эквивалентно существованию индекса i < length(l) с p(l[i], n+i).

LaTeX

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

Lean4

/-- Variant of `forall_mem_zipIdx` with the `zipIdx` argument specialized to `0`. -/
theorem forall_mem_zipIdx' {l : List α} {p : α × ℕ → Prop} :
    (∀ x ∈ l.zipIdx, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], i) :=
  forall_mem_zipIdx.trans <| by simp

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