DeZero.or_inl

Énoncé

∀ {a : Prop} {b : Prop} (ha : a), a ∨ b

Une preuve de a suffit à établir a ∨ b.

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

/-- Injection gauche. -/
theorem or_inl {a b : Prop} (ha : a) : a ∨ b :=
  Or.inl ha