length_le_iff — Mathlib

English

If s terminates, then s.length h ≤ n is equivalent to s.TerminatedAt n.

Русский

Если s завершается, то $s.length(h) \\le n\$ эквивалентно s.TerminatedAt n.

LaTeX

$$$s.length(h) \\le n \\iff s.TerminatedAt n$$$

Lean4

/-- The statement of `length_le_iff` assumes that the sequence terminates. For a
statement of the where the sequence is not known to terminate see `length_le_iff'`. -/
theorem length_le_iff {s : Seq α} {n : ℕ} {h : s.Terminates} : s.length h ≤ n ↔ s.TerminatedAt n := by
  rw [← length_le_iff']; simp [h]

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