DeZero.or_elim

Énoncé

∀ {a : Prop} {b : Prop} {c : Prop} (h : a ∨ b) (ha : a → c) (hb : b → c), c

Raisonnement par cas. Appliqué à la trichotomie, c’est lui qui ouvre les trois branches.

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

/-- Analyse de cas sur une disjonction. C'est ce bloc qui, appliqué à `ax6_trichotomie`,
donnera l'essentiel du raisonnement par cas sur l'ordre. -/
theorem or_elim {a b c : Prop} (h : a ∨ b) (ha : a → c) (hb : b → c) : c :=
  Or.rec (motive := fun _ => c) ha hb h