English
If s.get? n = some a_n, then there exists a_m with m ≤ n such that s.get? m = some a_m.
Русский
Если s.get? n = some a_n, то существует a_m с m ≤ n such что s.get? m = some a_m.
LaTeX
$$$\\forall s:\\mathrm{Seq}\\,\\alpha\\;\\forall n\\;\\exists m\\le n,\\;\\exists a_m:\\alpha,\\; s.\\mathrm{get?}(m)=\\mathrm{some}(a_m)\\land s.\\mathrm{get?}(n)=\\mathrm{some}(a_n).$$$
Lean4
/-- If `s.get? n = some aₙ` for some value `aₙ`, then there is also some value `aₘ` such
that `s.get? = some aₘ` for `m ≤ n`.
-/
theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n) (s_nth_eq_some : s.get? n = some aₙ) :
∃ aₘ : α, s.get? m = some aₘ :=
have : s.get? n ≠ none := by simp [s_nth_eq_some]
have : s.get? m ≠ none := mt (s.le_stable m_le_n) this
Option.ne_none_iff_exists'.mp this
