English
Let s ∈ Seq α, and n, m ∈ ℕ. If we update the nth element of s by f, then the m-th get? is as follows: equals (s.get? m).map f if m = n, else s.get? m.
Русский
Пусть s ∈ Seq α, n, m ∈ ℕ. Если обновить n-й элемент последовательности s с помощью f, то элемент m-й позиции будет равен (s.get? m).map f, если m = n; иначе s.get? m.
LaTeX
$$$(s.update\ n\ f).get?\ m = \begin{cases} (s.get?\ m).map\ f, & m = n \\ s.get?\ m, & m \neq n \end{cases}$$$
Lean4
theorem get?_update (s : Seq α) (n : ℕ) (m : ℕ) :
(s.update n f).get? m = if m = n then (s.get? m).map f else s.get? m :=
by
simp [update, Function.update]
split_ifs with h_if
· simp [h_if]
· rfl
