updateFinset — Mathlib

English

updateFinset x s y is the vector x with coordinates in s replaced by the values of y.

Русский

updateFinset x s y — вектор x, в котором координаты из s заменяются значениями y.

LaTeX

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

Lean4

/-- `updateFinset x s y` is the vector `x` with the coordinates in `s` changed to the values of `y`.
-/
def updateFinset (x : ∀ i, π i) (s : Finset ι) (y : ∀ i : ↥s, π i) (i : ι) : π i :=
  if hi : i ∈ s then y ⟨i, hi⟩ else x i

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