exists_mem_cons_iff — Mathlib

English

For any p, a, l, the statement ∃ x ∈ a :: l, p x is equivalent to p a ∨ ∃ x ∈ l, p x.

Русский

Для произвольных p, a, l верно: ∃ x ∈ a :: l, p x эквивалентно p a ∨ ∃ x ∈ l, p x.

LaTeX

$$$$\\forall \\alpha\\,(p:\\\\alpha \\\\to \\\\mathrm{Prop})\\,(a:\\\\alpha)\\,(l:\\\\mathrm{List}\\\\alpha), (\\\\Exists x \\\\in (a :: l),\\\\ p(x)) \\\\iff p(a) \\\\lor (\\\\Exists x \\\\in l,\\\\ p(x)).$$$$

Lean4

theorem exists_mem_cons_iff (p : α → Prop) (a : α) (l : List α) : (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x := by grind

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