get_set_eq_if — Mathlib

English

The value at j after setting i equals a if i = j and equals the original value otherwise.

Русский

Значение на позиции j после установки i равно a, если i = j, и иначе равно исходному значению.

LaTeX

$$$ (v.set i a).get j = \\text{if } i=j \\text{ then } a \\text{ else } v.get j $$$

Lean4

theorem get_set_eq_if {v : Vector α n} {i j : Fin n} (a : α) : (v.set i a).get j = if i = j then a else v.get j := by
  split_ifs <;> (try simp [*]); rwa [get_set_of_ne]

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