DeZero.iff_intro

Énoncé

∀ {a : Prop} {b : Prop} (hab : a → b) (hba : b → a), a ↔ b

Une équivalence se construit avec les deux implications.

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 l'équivalence, par les deux implications. -/
theorem iff_intro {a b : Prop} (hab : a → b) (hba : b → a) : a ↔ b :=
  Iff.intro hab hba