ite_ite_comm — Mathlib

English

Two nested ITEs commute under a suitable condition: (if p then a else if q then b else c) = if q then b else if p then a else c when p → ¬q.

Русский

Два вложенных условных оператора коммутируют при условии p → ¬q: ...

LaTeX

$$$\text{if } p \to \neg q \text{ then } (\text{if } p \text{ then } a \text{ else if } q \text{ then } b \text{ else } c) = (\text{if } q \text{ then } b \text{ else if } p \text{ then } a \text{ else } c)$$$

Lean4

theorem ite_ite_comm (h : P → ¬Q) : (if P then a else if Q then b else c) = if Q then b else if P then a else c :=
  dite_dite_comm P Q h

Похожие утверждения