mathlib documentation

core / init.propext

@[ext]
constant propext {a b : Prop} :
(a b)a = b
theorem forall_congr_eq {a : Sort u} {p q : a → Prop} (h : ∀ (x : a), p x = q x) :
(∀ (x : a), p x) = ∀ (x : a), q x
theorem imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) :
(a → b) = (c → d)
theorem imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) :
(a → b) = (c → d)
theorem eq_true_intro {a : Prop} (h : a) :
theorem eq_false_intro {a : Prop} (h : ¬a) :
theorem iff.to_eq {a b : Prop} (h : a b) :
a = b
theorem iff_eq_eq {a b : Prop} :
(a b) = (a = b)
theorem eq_false {a : Prop} :
a = false = ¬a
theorem eq_true {a : Prop} :
a = true = a