Exists.elim

Énoncé

∀ {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b), b

Pour se servir d’une existence, on nomme un témoin quelconque 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

Cette déclaration vient du cœur de Lean 4 (Init.Core) et non de ce dépôt. Elle figure dans la bibliothèque parce que la liste blanche du projet l’autorise.