Lemmas about booleans

These are the lemmas about booleans which were present in core Lean 3. See also the file Mathlib.Data.Bool.Basic which contains lemmas about booleans from mathlib 3.

theorem Bool.true_eq_false_eq_False : ¬true = false

theorem Bool.false_eq_true_eq_False : ¬false = true

theorem Bool.eq_false_eq_not_eq_true (b : Bool) : (¬b = true) = (b = false)

theorem Bool.eq_true_eq_not_eq_false (b : Bool) : (¬b = false) = (b = true)

theorem Bool.eq_false_of_not_eq_true {b : Bool} : ¬b = true → b = false

theorem Bool.eq_true_of_not_eq_false {b : Bool} : ¬b = false → b = true

theorem Bool.and_eq_true_eq_eq_true_and_eq_true (a : Bool) (b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

theorem Bool.or_eq_true_eq_eq_true_or_eq_true (a : Bool) (b : Bool) : ((a || b) = true) = (a = true ∨ b = true)

theorem Bool.not_eq_true_eq_eq_false (a : Bool) : ((!a) = true) = (a = false)

theorem Bool.and_eq_false_eq_eq_false_or_eq_false (a : Bool) (b : Bool) : ((a && b) = false) = (a = false ∨ b = false)

theorem Bool.or_eq_false_eq_eq_false_and_eq_false (a : Bool) (b : Bool) : ((a || b) = false) = (a = false ∧ b = false)

theorem Bool.not_eq_false_eq_eq_true (a : Bool) : ((!a) = false) = (a = true)

theorem Bool.coe_false : (false = true) = False

theorem Bool.coe_true : (true = true) = True

theorem Bool.coe_sort_false : (false = true) = False

theorem Bool.coe_sort_true : (true = true) = True

theorem Bool.decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p

theorem Bool.decide_true {p : Prop} [Decidable p] : p → decide p = true

theorem Bool.of_decide_true {p : Prop} [Decidable p] : decide p = true → p

theorem Bool.bool_iff_false {b : Bool} : ¬b = true ↔ b = false

theorem Bool.bool_eq_false {b : Bool} : ¬b = true → b = false

theorem Bool.decide_false_iff (p : Prop) : ∀ {x : Decidable p}, decide p = false ↔ ¬p

theorem Bool.decide_false {p : Prop} [Decidable p] : ¬p → decide p = false

theorem Bool.of_decide_false {p : Prop} [Decidable p] : decide p = false → ¬p

theorem Bool.decide_congr {p : Prop} {q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q

@[deprecated Bool.or_eq_true_iff]

theorem Bool.coe_or_iff (x : Bool) (y : Bool) : (x || y) = true ↔ x = true ∨ y = true

Alias of Bool.or_eq_true_iff.

@[deprecated Bool.and_eq_true_iff]

theorem Bool.coe_and_iff (x : Bool) (y : Bool) : (x && y) = true ↔ x = true ∧ y = true

Alias of Bool.and_eq_true_iff.

theorem Bool.coe_xor_iff (a : Bool) (b : Bool) : xor a b = true ↔ Xor' (a = true) (b = true)