get?_zero_eq_none — Mathlib

English

For any sequence s, get? 0 = none if and only if s = nil.

Русский

Для любой последовательности s, get? 0 = none тогда и только тогда, когда s = nil.

LaTeX

$$$\\forall s:\\mathrm{Seq}\\,\\alpha,\\; \\operatorname{get?}(s,0)=\\mathrm{none} \\iff s=\\mathrm{nil}$$$

Lean4

@[simp]
theorem get?_zero_eq_none {s : Seq α} : s.get? 0 = none ↔ s = nil :=
  by
  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
  ext1 n
  exact le_stable s (Nat.zero_le _) h

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