piecewise_insert — Mathlib

English

Inserting j into s yields a piecewise equal to updating by f(j) at j: (insert j s).piecewise f g = update (s.piecewise f g) j (f j).

Русский

Добавление j в s даёт piecewise, равное обновлению в точке j значением f(j).

LaTeX

$$$(\\mathrm{insert}\\ j\\ s).\\text{piecewise } f g = \\mathrm{update} (s.\\text{piecewise } f g)\\ j\\ (f\\ j).$$$

Lean4

theorem piecewise_insert [DecidableEq ι] (j : ι) [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g = update (s.piecewise f g) j (f j) :=
  by
  classical simp only [← piecewise_coe, ← Set.piecewise_insert]
  ext
  congr
  simp

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