mathlib3 documentation

core / init.data.bool.lemmas

@[simp]
theorem cond_a_a {α : Type u} (b : bool) (a : α) :
cond b a a = a
@[simp]
theorem band_self (b : bool) :
b && b = b
@[simp]
theorem band_tt (b : bool) :
@[simp]
theorem band_ff (b : bool) :
@[simp]
theorem tt_band (b : bool) :
@[simp]
theorem ff_band (b : bool) :
@[simp]
theorem bor_self (b : bool) :
b || b = b
@[simp]
theorem bor_tt (b : bool) :
@[simp]
theorem bor_ff (b : bool) :
@[simp]
theorem tt_bor (b : bool) :
@[simp]
theorem ff_bor (b : bool) :
@[simp]
theorem bxor_self (b : bool) :
@[simp]
theorem bxor_tt (b : bool) :
theorem bxor_ff (b : bool) :
@[simp]
theorem tt_bxor (b : bool) :
theorem ff_bxor (b : bool) :
@[simp]
theorem bnot_bnot (b : bool) :
!!b = b
@[simp]
theorem eq_ff_eq_not_eq_tt (b : bool) :
@[simp]
theorem eq_tt_eq_not_eq_ff (b : bool) :
@[simp]
@[simp]
@[simp]
theorem bnot_eq_true_eq_eq_ff (a : bool) :
@[simp]
@[simp]
@[simp]
theorem bnot_eq_ff_eq_eq_tt (a : bool) :
@[simp]
theorem coe_ff  :
@[simp]
theorem coe_tt  :
@[simp]
@[simp]
@[simp]
theorem to_bool_iff (p : Prop) [d : decidable p] :
theorem to_bool_true {p : Prop} [decidable p] :
theorem to_bool_tt {p : Prop} [decidable p] :
theorem of_to_bool_true {p : Prop} [decidable p] :
theorem bool_iff_false {b : bool} :
theorem bool_eq_false {b : bool} :
@[simp]
theorem to_bool_ff_iff (p : Prop) [decidable p] :
theorem to_bool_ff {p : Prop} [decidable p] :
theorem to_bool_congr {p q : Prop} [decidable p] [decidable q] (h : p q) :
@[simp]
theorem bor_coe_iff (a b : bool) :
(a || b) a b
@[simp]
theorem band_coe_iff (a b : bool) :
(a && b) a b
@[simp]
theorem bxor_coe_iff (a b : bool) :
@[simp]
theorem ite_eq_tt_distrib (c : Prop) [decidable c] (a b : bool) :
ite c a b = bool.tt = ite c (a = bool.tt) (b = bool.tt)
@[simp]
theorem ite_eq_ff_distrib (c : Prop) [decidable c] (a b : bool) :
ite c a b = bool.ff = ite c (a = bool.ff) (b = bool.ff)