dite_ite_distrib_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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