exists_mem_cons_of_exists — Mathlib

English

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

Русский

Если существует x с p(x) в списке l, тогда существует x с p(x) в списке a :: l.

LaTeX

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

Lean4

theorem exists_mem_cons_of_exists {p : α → Prop} {a : α} {l : List α} : (∃ x ∈ l, p x) → ∃ x ∈ a :: l, p x :=
  fun ⟨x, xl, px⟩ => ⟨x, mem_cons_of_mem _ xl, px⟩

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