any_iff_exists_prop — Mathlib

English

Let l be a list and p a predicate on α. The statement that some element of l satisfies p is equivalent to the existence of an element a such that a ∈ l and p(a).

Русский

Пусть l — список, а p — предикат на α. Существование элемента списка, удовлетворяющего p, эквивалентно существованию элемента a such that a ∈ l и p(a).

LaTeX

$$$$ (\exists a \in l,\ p(a)) \iff (\exists a,\ a \in l \land p(a)). $$$$

Lean4

theorem any_iff_exists_prop : (any l fun a => p a) ↔ ∃ a ∈ l, p a := by simp

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