mathlib docs: core.init.cc

source

theorem iff_eq_of_eq_true_left {a b : Prop} :

a = true → (a ↔ b) = b

source

theorem iff_eq_of_eq_true_right {a b : Prop} :

b = true → (a ↔ b) = a

source

theorem iff_eq_true_of_eq {a b : Prop} :

a = b → (a ↔ b) = true

source

theorem and_eq_of_eq_true_left {a b : Prop} :

a = true → (a ∧ b) = b

source

theorem and_eq_of_eq_true_right {a b : Prop} :

b = true → (a ∧ b) = a

source

theorem and_eq_of_eq_false_left {a b : Prop} :

a = false → (a ∧ b) = false

source

theorem and_eq_of_eq_false_right {a b : Prop} :

b = false → (a ∧ b) = false

source

theorem and_eq_of_eq {a b : Prop} :

a = b → (a ∧ b) = a

source

theorem or_eq_of_eq_true_left {a b : Prop} :

a = true → (a ∨ b) = true

source

theorem or_eq_of_eq_true_right {a b : Prop} :

b = true → (a ∨ b) = true

source

theorem or_eq_of_eq_false_left {a b : Prop} :

a = false → (a ∨ b) = b

source

theorem or_eq_of_eq_false_right {a b : Prop} :

b = false → (a ∨ b) = a

source

theorem or_eq_of_eq {a b : Prop} :

a = b → (a ∨ b) = a

source

theorem imp_eq_of_eq_true_left {a b : Prop} :

a = true → (a → b) = b

source

theorem imp_eq_of_eq_true_right {a b : Prop} :

b = true → (a → b) = true

source

theorem imp_eq_of_eq_false_left {a b : Prop} :

a = false → (a → b) = true

source

theorem imp_eq_of_eq_false_right {a b : Prop} :

b = false → (a → b) = ¬a

source

theorem not_imp_eq_of_eq_false_right {a b : Prop} :

b = false → (¬a → b) = a

source

theorem imp_eq_true_of_eq {a b : Prop} :

a = b → (a → b) = true

source

theorem not_eq_of_eq_true {a : Prop} :

a = true → (¬a) = false

source

theorem not_eq_of_eq_false {a : Prop} :

a = false → (¬a) = true

source

theorem false_of_a_eq_not_a {a : Prop} :

a = ¬a → false

source

theorem if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Sort u} (t e : α) :

c = true → ite c t e = t

source

theorem if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Sort u} (t e : α) :

c = false → ite c t e = e

source

theorem if_eq_of_eq (c : Prop) [d : decidable c] {α : Sort u} {t e : α} :

t = e → ite c t e = t

source

theorem eq_true_of_and_eq_true_left {a b : Prop} :

(a ∧ b) = true → a = true

source

theorem eq_true_of_and_eq_true_right {a b : Prop} :

(a ∧ b) = true → b = true

source

theorem eq_false_of_or_eq_false_left {a b : Prop} :

(a ∨ b) = false → a = false

source

theorem eq_false_of_or_eq_false_right {a b : Prop} :

(a ∨ b) = false → b = false

source

theorem eq_false_of_not_eq_true {a : Prop} :

(¬a) = true → a = false

source

theorem eq_true_of_not_eq_false {a : Prop} :

(¬a) = false → a = true

source

theorem ne_of_eq_of_ne {α : Sort u} {a b c : α} :

a = b → b ≠ c → a ≠ c

source

theorem ne_of_ne_of_eq {α : Sort u} {a b c : α} :

a ≠ b → b = c → a ≠ c

mathlib documentation

core.init.cc_lemmas

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​cc_lemmas

General documentation

Additional documentation

Library

core.init.cc_lemmas