mathlib documentation

core / init.ite_simp

source
@[simp]
theorem if_true_right_eq_or (p : Prop) [h : decidable p] (q : Prop) :
ite p q true = (¬p ∨ q)
source
@[simp]
theorem if_true_left_eq_or (p : Prop) [h : decidable p] (q : Prop) :
ite p true q = (p ∨ q)
source
@[simp]
theorem if_false_right_eq_and (p : Prop) [h : decidable p] (q : Prop) :
ite p q false = (p ∧ q)
source
@[simp]
theorem if_false_left_eq_and (p : Prop) [h : decidable p] (q : Prop) :
ite p false q = (¬p ∧ q)