mathlib docs: core.init.data.bool.lemmas

source

@[simp]

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

cond b a a = a

source

@[simp]

theorem band_self (b : bool) :

b && b = b

source

@[simp]

theorem band_tt (b : bool) :

b && bool.tt = b

source

@[simp]

theorem band_ff (b : bool) :

b && bool.ff = bool.ff

source

@[simp]

theorem tt_band (b : bool) :

bool.tt && b = b

source

@[simp]

theorem ff_band (b : bool) :

bool.ff && b = bool.ff

source

@[simp]

theorem bor_self (b : bool) :

b || b = b

source

@[simp]

theorem bor_tt (b : bool) :

b || bool.tt = bool.tt

source

@[simp]

theorem bor_ff (b : bool) :

b || bool.ff = b

source

@[simp]

theorem tt_bor (b : bool) :

bool.tt || b = bool.tt

source

@[simp]

theorem ff_bor (b : bool) :

bool.ff || b = b

source

@[simp]

theorem bxor_self (b : bool) :

bxor b b = bool.ff

source

@[simp]

theorem bxor_tt (b : bool) :

bxor b bool.tt = !b

source

@[simp]

theorem bxor_ff (b : bool) :

bxor b bool.ff = b

source

@[simp]

theorem tt_bxor (b : bool) :

bxor bool.tt b = !b

source

@[simp]

theorem ff_bxor (b : bool) :

bxor bool.ff b = b

source

@[simp]

theorem bnot_bnot (b : bool) :

!!b = b

source

@[simp]

theorem tt_eq_ff_eq_false :

¬bool.tt = bool.ff

source

@[simp]

theorem ff_eq_tt_eq_false :

¬bool.ff = bool.tt

source

@[simp]

theorem eq_ff_eq_not_eq_tt (b : bool) :

(¬b = bool.tt) = (b = bool.ff)

source

@[simp]

theorem eq_tt_eq_not_eq_ff (b : bool) :

(¬b = bool.ff) = (b = bool.tt)

source

theorem eq_ff_of_not_eq_tt {b : bool} :

¬b = bool.tt → b = bool.ff

source

theorem eq_tt_of_not_eq_ff {b : bool} :

¬b = bool.ff → b = bool.tt

source

@[simp]

theorem band_eq_true_eq_eq_tt_and_eq_tt (a b : bool) :

a && b = bool.tt = (a = bool.tt ∧ b = bool.tt)

source

@[simp]

theorem bor_eq_true_eq_eq_tt_or_eq_tt (a b : bool) :

a || b = bool.tt = (a = bool.tt ∨ b = bool.tt)

source

@[simp]

theorem bnot_eq_true_eq_eq_ff (a : bool) :

!a = bool.tt = (a = bool.ff)

source

@[simp]

theorem band_eq_false_eq_eq_ff_or_eq_ff (a b : bool) :

a && b = bool.ff = (a = bool.ff ∨ b = bool.ff)

source

@[simp]

theorem bor_eq_false_eq_eq_ff_and_eq_ff (a b : bool) :

a || b = bool.ff = (a = bool.ff ∧ b = bool.ff)

source

@[simp]

theorem bnot_eq_ff_eq_eq_tt (a : bool) :

!a = bool.ff = (a = bool.tt)

source

@[simp]

theorem coe_ff :

↑bool.ff = false

source

@[simp]

theorem coe_tt :

↑bool.tt = true

source

@[simp]

theorem coe_sort_ff :

↥bool.ff = false

source

@[simp]

theorem coe_sort_tt :

↥bool.tt = true

source

@[simp]

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

decidable.to_bool p = bool.tt ↔ p

source

theorem to_bool_true {p : Prop} [decidable p] :

p → ↥(decidable.to_bool p)

source

theorem to_bool_tt {p : Prop} [decidable p] :

p → decidable.to_bool p = bool.tt

source

theorem of_to_bool_true {p : Prop} [decidable p] :

↥(decidable.to_bool p) → p

source

theorem bool_iff_false {b : bool} :

¬↥b ↔ b = bool.ff

source

theorem bool_eq_false {b : bool} :

¬↥b → b = bool.ff

source

@[simp]

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

decidable.to_bool p = bool.ff ↔ ¬p

source

theorem to_bool_ff {p : Prop} [decidable p] :

¬p → decidable.to_bool p = bool.ff

source

theorem of_to_bool_ff {p : Prop} [decidable p] :

decidable.to_bool p = bool.ff → ¬p

source

theorem to_bool_congr {p q : Prop} [decidable p] [decidable q] :

(p ↔ q) → decidable.to_bool p = decidable.to_bool q

source

@[simp]

theorem bor_coe_iff (a b : bool) :

↥(a || b) ↔ ↥a ∨ ↥b

source

@[simp]

theorem band_coe_iff (a b : bool) :

↥(a && b) ↔ ↥a ∧ ↥b

source

@[simp]

theorem bxor_coe_iff (a b : bool) :

↥(bxor a b) ↔ xor ↥a ↥b

source

@[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)

source

@[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)

mathlib documentation

core.init.data.bool.lemmas

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​data.​bool.​lemmas

General documentation

Additional documentation

Library

core.init.data.bool.lemmas