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