mathlib3 documentation

core / init.cc_lemmas

Lemmas use by the congruence closure module

source
theorem iff_eq_of_eq_true_left {a b : Prop} (h : a = true) :
(a ↔ b) = b
source
theorem iff_eq_of_eq_true_right {a b : Prop} (h : b = true) :
(a ↔ b) = a
source
theorem iff_eq_true_of_eq {a b : Prop} (h : a = b) :
(a ↔ b) = true
source
theorem and_eq_of_eq_true_left {a b : Prop} (h : a = true) :
(a ∧ b) = b
source
theorem and_eq_of_eq_true_right {a b : Prop} (h : b = true) :
(a ∧ b) = a
source
theorem and_eq_of_eq_false_left {a b : Prop} (h : a = false) :
(a ∧ b) = false
source
theorem and_eq_of_eq_false_right {a b : Prop} (h : b = false) :
(a ∧ b) = false
source
theorem and_eq_of_eq {a b : Prop} (h : a = b) :
(a ∧ b) = a
source
theorem or_eq_of_eq_true_left {a b : Prop} (h : a = true) :
(a ∨ b) = true
source
theorem or_eq_of_eq_true_right {a b : Prop} (h : b = true) :
(a ∨ b) = true
source
theorem or_eq_of_eq_false_left {a b : Prop} (h : a = false) :
(a ∨ b) = b
source
theorem or_eq_of_eq_false_right {a b : Prop} (h : b = false) :
(a ∨ b) = a
source
theorem or_eq_of_eq {a b : Prop} (h : a = b) :
(a ∨ b) = a
source
theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = true) :
(a → b) = b
source
theorem imp_eq_of_eq_true_right {a b : Prop} (h : b = true) :
(a → b) = true
source
theorem imp_eq_of_eq_false_left {a b : Prop} (h : a = false) :
(a → b) = true
source
theorem imp_eq_of_eq_false_right {a b : Prop} (h : b = false) :
(a → b) = ¬a
source
theorem not_imp_eq_of_eq_false_right {a b : Prop} (h : b = false) :
(¬a → b) = a

Remark: the congruence closure module will only use this lemma if cc_config.em is tt.

source
theorem imp_eq_true_of_eq {a b : Prop} (h : a = b) :
(a → b) = true
source
theorem not_eq_of_eq_true {a : Prop} (h : a = true) :
(¬a) = false
source
theorem not_eq_of_eq_false {a : Prop} (h : a = false) :
(¬a) = true
source
theorem false_of_a_eq_not_a {a : Prop} (h : a = ¬a) :
false
source
theorem if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Sort u} (t e : α) (h : c = true) :
ite c t e = t
source
theorem if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Sort u} (t e : α) (h : c = false) :
ite c t e = e
source
theorem if_eq_of_eq (c : Prop) [d : decidable c] {α : Sort u} {t e : α} (h : t = e) :
ite c t e = t
source
theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = true) :
a = true
source
theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = true) :
b = true
source
theorem eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = false) :
a = false
source
theorem eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = false) :
b = false
source
theorem eq_false_of_not_eq_true {a : Prop} (h : (¬a) = true) :
a = false
source
theorem eq_true_of_not_eq_false {a : Prop} (h : (¬a) = false) :
a = true

Remark: the congruence closure module will only use this lemma if cc_config.em is tt.

source
theorem ne_of_eq_of_ne {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) :
a ≠ c
source
theorem ne_of_ne_of_eq {α : Sort u} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) :
a ≠ c