update_eq_piecewise — Mathlib

English

Update at i is the same as piecewise with singleton i in the left branch: update f i v = piecewise (singleton i) (λ _, v) f.

Русский

Обновление в позиции i равно piecewise со сконструированным слоем слева: update f i v = piecewise singleton i (λ _, v) f.

LaTeX

$$$\\text{update } f\\ i\\ v = \\text{piecewise}(\\text{singleton } i) (\\lambda x. v)\\ f.$$$

Lean4

theorem update_eq_piecewise {β : Type*} [DecidableEq ι] (f : ι → β) (i : ι) (v : β) :
    update f i v = piecewise (singleton i) (fun _ => v) f :=
  (piecewise_singleton (fun _ => v) _ _).symm

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