mathlib documentation

theorem cond_a_a {α : Type u} (b : bool) (a : α) :

theorem band_self (b : bool) :

theorem band_tt (b : bool) :

theorem band_ff (b : bool) :

theorem tt_band (b : bool) :

theorem ff_band (b : bool) :

theorem bor_self (b : bool) :

theorem bor_tt (b : bool) :

theorem bor_ff (b : bool) :

theorem tt_bor (b : bool) :

theorem ff_bor (b : bool) :

theorem bxor_self (b : bool) :

theorem bxor_tt (b : bool) :

theorem bxor_ff (b : bool) :

theorem tt_bxor (b : bool) :

theorem ff_bxor (b : bool) :

theorem bnot_bnot (b : bool) :

theorem tt_eq_ff_eq_false  :

theorem ff_eq_tt_eq_false  :

theorem eq_ff_eq_not_eq_tt (b : bool) :

theorem eq_tt_eq_not_eq_ff (b : bool) :

theorem eq_ff_of_not_eq_tt {b : bool} (a : ¬b = tt) :

theorem eq_tt_of_not_eq_ff {b : bool} (a : ¬b = ff) :

theorem band_eq_true_eq_eq_tt_and_eq_tt (a b : bool) :

theorem bor_eq_true_eq_eq_tt_or_eq_tt (a b : bool) :

theorem bnot_eq_true_eq_eq_ff (a : bool) :

theorem band_eq_false_eq_eq_ff_or_eq_ff (a b : bool) :

theorem bor_eq_false_eq_eq_ff_and_eq_ff (a b : bool) :

theorem bnot_eq_ff_eq_eq_tt (a : bool) :

theorem coe_ff  :

theorem coe_tt  :

theorem coe_sort_ff  :

theorem coe_sort_tt  :

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

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

theorem to_bool_tt {p : Prop} [decidable p] (a : p) :

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

theorem bool_iff_false {b : bool} :

theorem bool_eq_false {b : bool} (a : ¬↥b) :

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

theorem to_bool_ff {p : Prop} [decidable p] (a : ¬p) :

theorem of_to_bool_ff {p : Prop} [decidable p] (a : to_bool p = ff) :

theorem to_bool_congr {p q : Prop} [decidable p] [decidable q] (h : p ↔ q) :

theorem bor_coe_iff (a b : bool) :

theorem band_coe_iff (a b : bool) :

theorem bxor_coe_iff (a b : bool) :

theorem ite_eq_tt_distrib (c : Prop) [decidable c] (a b : bool) :

theorem ite_eq_ff_distrib (c : Prop) [decidable c] (a b : bool) :