lt_length_iff — Mathlib

English

For terminating sequences, n < length h is equivalent to existence of an element at position n.

Русский

Для завершающихся последовательностей выполнено: n < length(h) эквивалентно существованию элемента на позиции n.

LaTeX

$$$n < \mathrm{length}(h) \iff \exists a, a \in s.get? 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 lt_length_iff {s : Seq α} {n : ℕ} {h : s.Terminates} : n < s.length h ↔ ∃ a, a ∈ s.get? n := by
  rw [← lt_length_iff']; simp [h]

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