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} :
(∀ (x : a), p x = q x)((∀ (x : a), p x) = ∀ (x : a), q x)

theorem imp_congr_eq {a b c d : Prop} :
a = cb = d(a → b) = (c → d)

theorem imp_congr_ctx_eq {a b c d : Prop} :
a = c(c → b = d)(a → b) = (c → d)

theorem eq_true_intro {a : Prop} :
a → a = true

theorem eq_false_intro {a : Prop} :
¬a → a = false

theorem iff.to_eq {a b : Prop} :
(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