DeZero.exists_elim

Énoncé

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

Pour se servir d’une existence, on nomme un témoin et on montre que la conclusion suit.

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

/-- Élimination de l'existentielle : on nomme le témoin et on conclut. -/
theorem exists_elim {α : Sort u} {p : α → Prop} {b : Prop} (h : ∃ x, p x)
    (f : ∀ w, p w → b) : b :=
  Exists.rec (motive := fun _ => b) f h