ite_dite_distrib_left — Mathlib

English

A distributive law relates 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)) (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)),\text{ite}(p,a,c(hq))) $$$

Lean4

theorem ite_dite_distrib_left {a : α} {b : q → α} {c : ¬q → α} :
    ite p a (dite q b c) = dite q (fun hq ↦ ite p a <| b hq) fun hq ↦ ite p a <| c hq :=
  dite_dite_distrib_left

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