updateFinset_def — Mathlib

English

updateFinset x s y is the function i ↦ if i ∈ s then y ⟨i, hi⟩ else x i.

Русский

updateFinset x s y — это функция i ↦ если i ∈ s, то y ⟨i, hi⟩, иначе x i.

LaTeX

$$$\\text{updateFinset}\\;x\\;s\\;y = \\lambda i. \\text{if } i\\in s \\text{ then } y\\langle i, hi \\rangle \\text{ else } x(i).$$$

Lean4

theorem updateFinset_def {s : Finset ι} {y} : updateFinset x s y = fun i ↦ if hi : i ∈ s then y ⟨i, hi⟩ else x i :=
  rfl

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