getElem_set_of_ne — Mathlib

English

If i ≠ j and a ∈ α, and j is a valid index in l.set i a, then (l.set i a)[j] = l[j].

Русский

Если i ≠ j и a ∈ α, и j допустимый индекс в списка l с заменой i-го элемента на a, то (l.set i a)[j] = l[j].

LaTeX

$$$\\\\forall l:\\\\, \\text{List }\\\\alpha,\\\\, \\forall i,j:\\\\mathbb{N},\\\\, i \\\\neq j \\\\Rightarrow \\\\forall a:\\\\alpha,\\\\, hj : j < (l.set i a).length \\\\Rightarrow (l.set i a)[j] = l[j].$$$

Lean4

theorem getElem_set_of_ne {l : List α} {i j : ℕ} (h : i ≠ j) (a : α) (hj : j < (l.set i a).length) :
    (l.set i a)[j] = l[j]'(by simpa using hj) := by simp [h]

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