Or.elim

Énoncé

∀ {a : Prop} {b : Prop} {c : Prop} (h : a ∨ b) (left : a → c) (right : b → c), c

Raisonnement par cas : si chacune des deux branches mène à la même conclusion, la disjonction y mène aussi.

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.Prelude) et non de ce dépôt. Elle figure dans la bibliothèque parce que la liste blanche du projet l’autorise.