piecewise_erase_univ — Mathlib

English

Removing an index i from the universal set yields the piecewise function that equals update f i (g i) on i and agrees with f elsewhere.

Русский

Удаление индекса i из вселенной даёт кусочно-заданную функцию, которая совпадает с обновлением f на i и равна g на i? (на i значение становится g i).

LaTeX

$$$$ (\\mathrm{univ} \\setminus \\{i\\}) .\\text{piecewise } f g = \\operatorname{update} f i (g i). $$$$

Lean4

@[simp]
theorem piecewise_erase_univ [DecidableEq ι] (i : ι) (f g : ∀ i, π i) :
    (Finset.univ.erase i).piecewise f g = Function.update f i (g i) := by
  rw [← compl_singleton, piecewise_compl, piecewise_singleton]

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