ite_dite_distrib_right — Mathlib

English

A distributive law relates ite and dite on the right: ite p (dite q a b) c equals dite q (λhq, ite p (a hq) c) (λhq, ite p (b hq) c).

Русский

Существуют распределения между ite и dite справа: ite p (dite q a b) c = dite q (λhq, ite p (a hq) c) (λhq, ite p (b hq) c).

LaTeX

$$$ \text{ite}(p,\text{dite}(q,a,b),c) = \text{dite}(q,\lambda hq.\text{ite}(p, a(hq), c), \lambda hq.\text{ite}(p, b(hq), c)) $$$

Lean4

theorem ite_dite_distrib_right {a : q → α} {b : ¬q → α} {c : α} :
    ite p (dite q a b) c = dite q (fun hq ↦ ite p (a hq) c) fun hq ↦ ite p (b hq) c :=
  dite_dite_distrib_right

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