not_terminates_iff — Mathlib

English

A sequence does not terminate if and only if every get? n is Some (i.e., exists a value at every position).

Русский

Последовательность не заканчивается тогда и только тогда, когда для каждого n элемент существует (Some).

LaTeX

$$$\\neg s.Terminates \\iff \\forall n, (s.get? n).isSome$$$

Lean4

theorem not_terminates_iff {s : Seq α} : ¬s.Terminates ↔ ∀ n, (s.get? n).isSome := by
  simp only [Terminates, TerminatedAt, ← Ne.eq_def, Option.ne_none_iff_isSome, not_exists, iff_self]

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