mathlib3 documentation

core / init.ite_simp

Simplification lemmas for ite. #

We don't prove them at logic.lean because it is easier to prove them using the tactic framework.

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)