DeZero.exists_intro

Énoncé

∀ {α : Sort u} {p : α → Prop} (w : α) (h : p w), ∃ x, p x

Pour établir une existence, il suffit d’exhiber un témoin.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

/-- Introduction de l'existentielle : un témoin et une preuve. -/
theorem exists_intro {α : Sort u} {p : α → Prop} (w : α) (h : p w) : ∃ x, p x :=
  Exists.intro w h