update_piecewise_of_notMem — Mathlib

English

If i is not a member of s, then updating the piecewise function at i by v affects only the right branch: update(s.piecewise f g) i v = s.piecewise f (update g i v).

Русский

Если i не входит в s, обновление по i влияет только на правую ветвь: update(s.piecewise f g) i v = s.piecewise f (update g i v).

LaTeX

$$$$\\text{If } i \\notin s,\\quad update\\bigl(s.piecewise f g\\bigr) i v = s.piecewise f\\bigl( update\\ g\\ i\\ v \\bigr).$$$$

Lean4

theorem update_piecewise_of_notMem [DecidableEq ι] {i : ι} (hi : i ∉ s) (v : π i) :
    update (s.piecewise f g) i v = s.piecewise f (update g i v) :=
  by
  rw [update_piecewise]
  refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl
  exact fun h => hi (h ▸ hj)

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