or_exists_of_exists_mem_cons — Mathlib

English

If there exists x with p(x) in a :: l, then either p(a) or there exists x with p(x) in l.

Русский

Если существует x с p(x) в a :: l, то либо p(a), либо существует x с p(x) в l.

LaTeX

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

Lean4

theorem or_exists_of_exists_mem_cons {p : α → Prop} {a : α} {l : List α} : (∃ x ∈ a :: l, p x) → p a ∨ ∃ x ∈ l, p x :=
  by grind

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