get?_set_of_not_terminatedAt — Mathlib

English

If n is not terminated in s, then (s.set n x).get? n = x.

Русский

Если n не достигнут терминатором в s, то (s.set n x).get? n = x.

LaTeX

$${s : Seq α} {n : ℕ} (h_not_terminated : ¬s.TerminatedAt n) : (s.set n x).get? n = x$$

Lean4

theorem get?_set_of_not_terminatedAt {s : Seq α} {n : ℕ} (h_not_terminated : ¬s.TerminatedAt n) :
    (s.set n x).get? n = x := by simpa [set, update, ← Option.ne_none_iff_exists'] using h_not_terminated

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