DeZero.iff_mpr

Énoncé

∀ {a : Prop} {b : Prop} (h : a ↔ b) (hb : b), a

D’une équivalence et de son membre droit, tire le membre gauche.

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

/-- Sens réciproque d'une équivalence. -/
theorem iff_mpr {a b : Prop} (h : a ↔ b) (hb : b) : a :=
  Iff.rec (motive := fun _ => a) (fun _ hba => hba hb) h