English
The statement length_le_iff' does not assume termination; it relates existence of a bound on length to termination at n.
Русский
Утверждение length_le_iff' не предполагает завершения; оно связывает существование границы длины с завершением на n.
LaTeX
$$$(\exists h, s.length h \le n) \iff s.TerminatedAt n$$$
Lean4
/-- The statement of `length_le_iff'` does not assume that the sequence terminates. For a
simpler statement of the theorem where the sequence is known to terminate see `length_le_iff`. -/
theorem length_le_iff' {s : Seq α} {n : ℕ} : (∃ h, s.length h ≤ n) ↔ s.TerminatedAt n :=
by
simp only [length, Nat.find_le_iff, TerminatedAt, Terminates, exists_prop]
refine ⟨?_, ?_⟩
· rintro ⟨_, k, hkn, hk⟩
exact le_stable s hkn hk
· intro hn
exact ⟨⟨n, hn⟩, ⟨n, le_rfl, hn⟩⟩
