← Copula mathematical handbook

Conditionals on a disjunction

Small rewriting lemmas for if p ∨ q then x else y, stated for an arbitrary decidability instance so that rw unifies with whatever instance the surrounding definition uses.

theorem ProbabilityTheory.Copula.ite_or_of_not {α : Sort u_1} {p q : Prop} {inst : Decidable (p ∨ q)} (hp : ¬p) (hq : ¬q) (x y : α) : (if p ∨ q then x else y) = y

theorem ProbabilityTheory.Copula.ite_or_of_left {α : Sort u_1} {p q : Prop} {inst : Decidable (p ∨ q)} (hp : p) (x y : α) : (if p ∨ q then x else y) = x

theorem ProbabilityTheory.Copula.ite_or_of_right {α : Sort u_1} {p q : Prop} {inst : Decidable (p ∨ q)} (hq : q) (x y : α) : (if p ∨ q then x else y) = x