terminatedAt_zero_iff — Mathlib

English

A sequence terminates at 0 if and only if the sequence is nil.

Русский

Последовательность завершается в позиции 0 тогда и только тогда, когда последовательность равна nil.

LaTeX

$$$ s.TerminatedAt(0) \\iff s = \\mathrm{nil} $$$

Lean4

theorem terminatedAt_zero_iff {s : Seq α} : s.TerminatedAt 0 ↔ s = nil :=
  by
  refine ⟨?_, ?_⟩
  · intro h
    ext n
    rw [le_stable _ (Nat.zero_le _) h]
    simp
  · rintro rfl
    simp [TerminatedAt]

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