English
The relation "n < length'(s)" is equivalent to the existence of an element at position n in s.
Русский
Отношение «n меньше length'(s)» эквивалентно существованию элемента на позиции n в s.
LaTeX
$$$n < \mathrm{length}'(s) \iff \exists a, a \in s.get? n$$$
Lean4
/-- The statement of `lt_length_iff'` does not assume that the sequence terminates. For a
simpler statement of the theorem where the sequence is known to terminate see `lt_length_iff`. -/
theorem lt_length_iff' {s : Seq α} {n : ℕ} : (∀ h : s.Terminates, n < s.length h) ↔ ∃ a, a ∈ s.get? n :=
by
simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
← Option.ne_none_iff_exists', ne_eq]
refine ⟨?_, ?_⟩
· intro h hn
exact h n hn n le_rfl hn
· intro hn _ _ k hkn hk
exact hn <| le_stable s hkn hk
