getElem?_take — Mathlib

English

If for all terminating h we have n ≤ length h, then (s.take n).length = n.

Русский

Если для всех завершающихся h имеет место n ≤ length h, то (s.take n).length = n.

LaTeX

$$$\mathrm{length}(\mathrm{take}(n, s)) = n$$$

Lean4

@[simp]
theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α), (s.take k)[n]? = if n < k then s.get? n else none
  | n, 0, s => by simp [take]
  | n, k + 1, s => by
    rw [take]
    cases h : destruct s with
    | none => simp [destruct_eq_none h]
    | some a =>
      match a with
      | (x, r) =>
        rw [destruct_eq_cons h]
        match n with
        | 0 => simp
        | n + 1 => simp [List.getElem?_cons_succ, getElem?_take]

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