dite_ite_distrib_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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