mathlib documentation

core / init.ite_simp

@[simp]
theorem if_true_right_eq_or (p : Prop) [h : decidable p] (q : Prop) :
ite p q true = (¬p q)

@[simp]
theorem if_true_left_eq_or (p : Prop) [h : decidable p] (q : Prop) :
ite p true q = (p q)

@[simp]
theorem if_false_right_eq_and (p : Prop) [h : decidable p] (q : Prop) :
ite p q false = (p q)

@[simp]
theorem if_false_left_eq_and (p : Prop) [h : decidable p] (q : Prop) :
ite p false q = (¬p q)