Documentation

Mathlib.Init.Data.Bool.Lemmas

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.

@[simp]
theorem Bool.cond_true {α : Type u} {a : α} {b : α} :
(bif true then a else b) = a
@[simp]
theorem Bool.cond_false {α : Type u} {a : α} {b : α} :
(bif false then a else b) = b
@[simp]
theorem Bool.cond_self {α : Type u} (b : Bool) (a : α) :
(bif b then a else a) = a
@[simp]
theorem Bool.xor_self (b : Bool) :
xor b b = false
@[simp]
theorem Bool.xor_true (b : Bool) :
xor b true = !b
@[simp]
theorem Bool.true_xor (b : Bool) :
xor true b = !b
theorem Bool.decide_true {p : Prop} [inst : Decidable p] :
pdecide p = true
theorem Bool.of_decide_true {p : Prop} [inst : Decidable p] :
decide p = truep
theorem Bool.decide_false {p : Prop} [inst : Decidable p] :
¬pdecide p = false
theorem Bool.of_decide_false {p : Prop} [inst : Decidable p] :
decide p = false¬p
theorem Bool.decide_congr {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] (h : p q) :
theorem Bool.or_coe_iff (a : Bool) (b : Bool) :
(a || b) = true a = true b = true
theorem Bool.and_coe_iff (a : Bool) (b : Bool) :
(a && b) = true a = true b = true
@[simp]
theorem Bool.xor_coe_iff (a : Bool) (b : Bool) :
xor a b = true Xor' (a = true) (b = true)
@[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
@[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