length'_le_iff — Mathlib

English

If s terminates, then length' s ≤ n iff s.TerminatedAt n.

Русский

Если s завершается, то length' s ≤ n тогда и только тогда, когда s.TerminatedAt n.

LaTeX

$$$\mathrm{length}'(s) \le n \iff s.TerminatedAt n$$$

Lean4

theorem length'_le_iff {s : Seq α} {n : ℕ} : s.length' ≤ n ↔ s.TerminatedAt n :=
  by
  by_cases h : s.Terminates
  · simpa [length'_of_terminates h] using length_le_iff
  · simpa [length'_of_not_terminates h] using forall_not_of_not_exists h n

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