piecewise_insert — Mathlib

English

Inserting j into s yields piecewise on insert j s equal to update of piecewise on s at j with f(j).

Русский

При вставке j в s получаем равенство: piecewise на insert j s равняется обновлению на j от piecewise на s с значением f(j).

LaTeX

$$$\\text{piecewise}_{\\text{insert}(j,s)}(f,g) = \\text{update}_j\\bigl(\\text{piecewise}_s(f,g)\\bigr)$$$

Lean4

theorem piecewise_insert [DecidableEq α] (j : α) [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j) :=
  by
  simp +unfoldPartialApp only [piecewise, mem_insert_iff]
  ext i
  by_cases h : i = j
  · rw [h]
    simp
  · by_cases h' : i ∈ s <;> simp [h, h']

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