ite_ite_distrib_left — Mathlib

English

There is a distributive law for ite and dite on the left: ite p a (dite q b c) equals dite q (fun hq => ite p a (b hq)) (ite p a (c hq)).

Русский

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

LaTeX

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

Lean4

theorem ite_ite_distrib_left : ite p a (ite q b c) = ite q (ite p a b) (ite p a c) :=
  dite_dite_distrib_left

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