English
Let l be a finite list and p a property on its elements. Then there exists x in l with p(x) if and only if there exists an index i with i < length(l) such that p(l[i]).
Русский
Пусть l — конечный список и p — свойство над его элементами. Существует элемент x внутри l such that p(x) тогда и только тогда, когда существует индекс i, такой что i < длина(l) и p(l[i]).
LaTeX
$$$ (\exists x \in l,\; p\,x) \quad\longleftrightarrow\quad \exists i : \mathbb{N}, i < |l| \wedge p(l[i]) $$$
Lean4
theorem exists_mem_iff_getElem {l : List α} {p : α → Prop} : (∃ x ∈ l, p x) ↔ ∃ (i : ℕ) (_ : i < l.length), p l[i] :=
by
simp only [mem_iff_getElem]
exact ⟨fun ⟨_x, ⟨i, hi, hix⟩, hxp⟩ ↦ ⟨i, hi, hix ▸ hxp⟩, fun ⟨i, hi, hp⟩ ↦ ⟨_, ⟨i, hi, rfl⟩, hp⟩⟩
