piecewise_insert_of_ne — Mathlib

English

If i is different from j, inserting j into s does not change the i-component of the piecewise function: (insert j s).piecewise f g i = s.piecewise f g i.

Русский

Если i ≠ j, добавление j в s не изменяет значение на i в piecewise: (insert j s).piecewise f g i = s.piecewise f g i.

LaTeX

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

Lean4

@[simp]
theorem piecewise_insert_of_ne [DecidableEq ι] {i j : ι} [∀ i, Decidable (i ∈ insert j s)] (h : i ≠ j) :
    (insert j s).piecewise f g i = s.piecewise f g i := by simp [piecewise, h]

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