lt_length'_iff — Mathlib

English

For nonterminating sequences, n < length'(s) is equivalent to existence of an element at position n in s.

Русский

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

LaTeX

$$$n < \mathrm{length}'(s) \iff \exists a, a \in s.get? n$$$

Lean4

theorem lt_length'_iff {s : Seq α} {n : ℕ} : n < s.length' ↔ ∃ a, a ∈ s.get? n :=
  by
  by_cases h : s.Terminates
  · simpa [length'_of_terminates h] using lt_length_iff
  · simp only [length'_of_not_terminates h, ENat.coe_lt_top, Option.mem_def, true_iff]
    rw [not_terminates_iff] at h
    rw [← Option.isSome_iff_exists]
    exact h n

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