get_set_of_ne — Mathlib

English

If i ≠ j, then replacing i-th element with a does not affect the j-th element.

Русский

Если i ≠ j, то замена i-й позиции на a не влияет на j-ю позицию.

LaTeX

$$$ (v.set i a).get j = v.get j \\\\text{when } i ≠ j $$$

Lean4

theorem get_set_of_ne {v : Vector α n} {i j : Fin n} (h : i ≠ j) (a : α) : (v.set i a).get j = v.get j :=
  by
  cases v; cases i; cases j
  simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]
  rw [List.getElem_set_of_ne]
  · simpa using h

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