core / init.propext - mathlib3 docs

@[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)

mathlib3 documentation