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.

source

ink

@[simp]

theorem Bool.cond_true {α : Type u} {a : α} {b : α} :

(bif true then a else b) = a

source

ink

@[simp]

theorem Bool.cond_false {α : Type u} {a : α} {b : α} :

(bif false then a else b) = b

source

ink

@[simp]

theorem Bool.cond_self {α : Type u} (b : Bool) (a : α) :

(bif b then a else a) = a

source

ink

@[simp]

theorem Bool.xor_self (b : Bool) :

xor b b = false

source

ink

@[simp]

theorem Bool.xor_true (b : Bool) :

xor b true = !b

source

ink

theorem Bool.xor_false (b : Bool) :

xor b false = b

source

ink

@[simp]

theorem Bool.true_xor (b : Bool) :

xor true b = !b

source

ink

theorem Bool.false_xor (b : Bool) :

xor false b = b

source

ink

theorem Bool.true_eq_false_eq_False :

¬true = false

source

ink

theorem Bool.false_eq_true_eq_False :

¬false = true

source

ink

theorem Bool.eq_false_eq_not_eq_true (b : Bool) :

(¬b = true) = (b = false)

source

ink

theorem Bool.eq_true_eq_not_eq_false (b : Bool) :

(¬b = false) = (b = true)

source

ink

theorem Bool.eq_false_of_not_eq_true {b : Bool} :

¬b = true → b = false

source

ink

theorem Bool.eq_true_of_not_eq_false {b : Bool} :

¬b = false → b = true

source

ink

theorem Bool.and_eq_true_eq_eq_true_and_eq_true (a : Bool) (b : Bool) :

((a && b) = true) = (a = true ∧ b = true)

source

ink

theorem Bool.or_eq_true_eq_eq_true_or_eq_true (a : Bool) (b : Bool) :

((a || b) = true) = (a = true ∨ b = true)

source

ink

theorem Bool.not_eq_true_eq_eq_false (a : Bool) :

((!a) = true) = (a = false)

source

ink

@[simp]

theorem Bool.and_eq_false_eq_eq_false_or_eq_false (a : Bool) (b : Bool) :

((a && b) = false) = (a = false ∨ b = false)

source

ink

@[simp]

theorem Bool.or_eq_false_eq_eq_false_and_eq_false (a : Bool) (b : Bool) :

((a || b) = false) = (a = false ∧ b = false)

source

ink

theorem Bool.not_eq_false_eq_eq_true (a : Bool) :

((!a) = false) = (a = true)

source

ink

theorem Bool.coe_false :

(false = true) = False

source

ink

theorem Bool.coe_true :

(true = true) = True

source

ink

theorem Bool.coe_sort_false :

(false = true) = False

source

ink

theorem Bool.coe_sort_true :

(true = true) = True

source

ink

theorem Bool.decide_iff (p : Prop) [d : Decidable p] :

decide p = true ↔ p

source

ink

theorem Bool.decide_true {p : Prop} [inst : Decidable p] :

p → decide p = true

source

ink

theorem Bool.of_decide_true {p : Prop} [inst : Decidable p] :

decide p = true → p

source

ink

theorem Bool.bool_iff_false {b : Bool} :

¬b = true ↔ b = false

source

ink

theorem Bool.bool_eq_false {b : Bool} :

¬b = true → b = false

source

ink

theorem Bool.decide_false_iff (p : Prop) [inst : Decidable p] :

decide p = false ↔ ¬p

source

ink

theorem Bool.decide_false {p : Prop} [inst : Decidable p] :

¬p → decide p = false

source

ink

theorem Bool.of_decide_false {p : Prop} [inst : Decidable p] :

decide p = false → ¬p

source

ink

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

decide p = decide q

source

ink

theorem Bool.or_coe_iff (a : Bool) (b : Bool) :

(a || b) = true ↔ a = true ∨ b = true

source

ink

theorem Bool.and_coe_iff (a : Bool) (b : Bool) :

(a && b) = true ↔ a = true ∧ b = true

source

ink

@[simp]

theorem Bool.xor_coe_iff (a : Bool) (b : Bool) :

xor a b = true ↔ Xor' (a = true) (b = true)

source

ink

@[simp]

theorem Bool.ite_eq_true_distrib (c : Prop) [inst : Decidable c] (a : Bool) (b : Bool) :

((if c then a else b) = true) = if c then a = true else b = true

source

ink

@[simp]

theorem Bool.ite_eq_false_distrib (c : Prop) [inst : Decidable c] (a : Bool) (b : Bool) :

((if c then a else b) = false) = if c then a = false else b = false