set — Mathlib

English

Set s at index n to a, i.e., replace the nth element by a if it exists; otherwise s is unchanged.

Русский

Заменить n-й элемент последовательности на a, если он существует; иначе последовательность не изменяется.

LaTeX

$$$ \mathrm{set}(s,n,a) = \mathrm{update}(s,n\,\text{(λ_. a)},$) где элемент существует.$$

Lean4

/-- Sets the value of sequence `s` at index `n` to `a`. If the `n`th element does not exist
(`s` terminates earlier), the sequence is left unchanged. -/
def set (s : Seq α) (n : ℕ) (a : α) : Seq α :=
  update s n fun _ ↦ a

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