DeZero.and_intro

Énoncé

∀ {a : Prop} {b : Prop} (ha : a) (hb : b), a ∧ b

Assemble une preuve de a et une preuve de b en une preuve de 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

/-- Introduction de la conjonction. -/
theorem and_intro {a b : Prop} (ha : a) (hb : b) : a ∧ b :=
  And.intro ha hb