enumerate_eq_none — Mathlib

English

If sel(s) = none, then for all n, Enumerate(sel)(s,n) = none.

Русский

Если sel(s) = none, то для любых n, Enumerate(sel)(s,n) = none.

LaTeX

$$$\forall n, \operatorname{Enumerate}_{sel}(s,n) = \mathrm{none}$, given $sel(s) = \mathrm{none}$$$

Lean4

theorem enumerate_eq_none : ∀ {s n₁ n₂}, enumerate sel s n₁ = none → n₁ ≤ n₂ → enumerate sel s n₂ = none
  | _, 0, _ => fun h _ ↦ enumerate_eq_none_of_sel sel h
  | s, n + 1, m => fun h hm ↦ by
    cases hs : sel s
    · exact enumerate_eq_none_of_sel sel hs
    ·
      cases m with
      | zero => contradiction
      | succ m' =>
        simp only [enumerate, hs] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm

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