forall_mem_iff_getElem — Mathlib

English

Let l be a list and p a property on its elements. Then (for all x in l, p(x)) holds if and only if for every index i with i < length(l), p(l[i]) holds.

Русский

Пусть l — список и p — свойство над его элементами. Тогда ∀ x ∈ l, p(x) эквивалентно ∀ i < length(l), p(l[i]).

LaTeX

$$$ (\forall x \in l,\; p\,x) \quad\longleftrightarrow\quad \forall i : \mathbb{N},\; i < |l| \rightarrow p(l[i]) $$$

Lean4

theorem forall_mem_iff_getElem {l : List α} {p : α → Prop} : (∀ x ∈ l, p x) ↔ ∀ (i : ℕ) (_ : i < l.length), p l[i] := by
  simp [mem_iff_getElem, @forall_swap α]

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