mathlib 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) :
b && tt = b

@[simp]
theorem band_ff (b : bool) :
b && ff = ff

@[simp]
theorem tt_band (b : bool) :
tt && b = b

@[simp]
theorem ff_band (b : bool) :
ff && b = ff

@[simp]
theorem bor_self (b : bool) :
b || b = b

@[simp]
theorem bor_tt (b : bool) :
b || tt = tt

@[simp]
theorem bor_ff (b : bool) :
b || ff = b

@[simp]
theorem tt_bor (b : bool) :
tt || b = tt

@[simp]
theorem ff_bor (b : bool) :
ff || b = b

@[simp]
theorem bxor_self (b : bool) :
bxor b b = ff

@[simp]
theorem bxor_tt (b : bool) :
bxor b tt = !b

@[simp]
theorem bxor_ff (b : bool) :
bxor b ff = b

@[simp]
theorem tt_bxor (b : bool) :
bxor tt b = !b

@[simp]
theorem ff_bxor (b : bool) :
bxor ff b = b

@[simp]
theorem bnot_bnot (b : bool) :
!!b = b

@[simp]
theorem tt_eq_ff_eq_false  :

@[simp]
theorem ff_eq_tt_eq_false  :

@[simp]
theorem eq_ff_eq_not_eq_tt (b : bool) :
(¬b = tt) = (b = ff)

@[simp]
theorem eq_tt_eq_not_eq_ff (b : bool) :
(¬b = ff) = (b = tt)

theorem eq_ff_of_not_eq_tt {b : bool} :
¬b = ttb = ff

theorem eq_tt_of_not_eq_ff {b : bool} :
¬b = ffb = tt

@[simp]
theorem band_eq_true_eq_eq_tt_and_eq_tt (a b : bool) :
a && b = tt = (a = tt b = tt)

@[simp]
theorem bor_eq_true_eq_eq_tt_or_eq_tt (a b : bool) :
a || b = tt = (a = tt b = tt)

@[simp]
theorem bnot_eq_true_eq_eq_ff (a : bool) :
!a = tt = (a = ff)

@[simp]
theorem band_eq_false_eq_eq_ff_or_eq_ff (a b : bool) :
a && b = ff = (a = ff b = ff)

@[simp]
theorem bor_eq_false_eq_eq_ff_and_eq_ff (a b : bool) :
a || b = ff = (a = ff b = ff)

@[simp]
theorem bnot_eq_ff_eq_eq_tt (a : bool) :
!a = ff = (a = tt)

@[simp]
theorem coe_ff  :

@[simp]
theorem coe_tt  :

@[simp]
theorem coe_sort_ff  :

@[simp]
theorem coe_sort_tt  :

@[simp]
theorem to_bool_iff (p : Prop) [d : decidable p] :

theorem to_bool_true {p : Prop} [decidable p] :
p → (to_bool p)

theorem to_bool_tt {p : Prop} [decidable p] :
p → to_bool p = tt

theorem of_to_bool_true {p : Prop} [decidable p] :
(to_bool p) → p

theorem bool_iff_false {b : bool} :

theorem bool_eq_false {b : bool} :
¬b → b = ff

@[simp]
theorem to_bool_ff_iff (p : Prop) [decidable p] :

theorem to_bool_ff {p : Prop} [decidable p] :
¬p → to_bool p = ff

theorem of_to_bool_ff {p : Prop} [decidable p] :
to_bool p = ff¬p

theorem to_bool_congr {p q : Prop} [decidable p] [decidable q] :
(p q)to_bool p = to_bool 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 = tt = ite c (a = tt) (b = tt)

@[simp]
theorem ite_eq_ff_distrib (c : Prop) [decidable c] (a b : bool) :
ite c a b = ff = ite c (a = ff) (b = ff)