exists_mem_cons_of — Mathlib

English

Let p be a predicate on elements of the type. If p(a) holds for some a, then there exists an element x in the list a :: l such that p(x).

Русский

Пусть p — предикат на элементы множества. Если выполняется p(a) для некоторого a, то существует элемент x в списке a :: l such that p(x).

LaTeX

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

Lean4

theorem exists_mem_cons_of {p : α → Prop} {a : α} (l : List α) (h : p a) : ∃ x ∈ a :: l, p x :=
  ⟨a, mem_cons_self, h⟩

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