ite_ite_distrib_right — Mathlib

English

There is a distributive law for ite and dite on the right: ite p (dite q a b) c equals dite q (fun hq => ite p (a hq) c) (fun 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_ite_distrib_right : ite p (ite q a b) c = ite q (ite p a c) (ite p b c) :=
  dite_dite_distrib_right

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