le_stable — Mathlib

English

If m ≤ n and s.get? m = none, then s.get? n = none.

Русский

Если m ≤ n и s.get? m = none, то s.get? n = none.

LaTeX

$$$\\forall s:\\mathrm{Seq}\\,\\alpha\\;\\forall m\\forall n\\;(m\\le n)\\;\\big(s.\\mathrm{get?}(m)=\\mathrm{none}\\Rightarrow s.\\mathrm{get?}(n)=\\mathrm{none}\\big).$$$

Lean4

theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get? n = none :=
  by
  obtain ⟨f, al⟩ := s
  induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)

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