length_take_le — Mathlib

English

A variant of length_take_of_le_length: (s.take n).length = n under suitable conditions.

Русский

Вариант утверждения о длине выборки: длина (take n) равна n при подходящих условиях.

LaTeX

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

Lean4

theorem length_take_le {s : Seq α} {n : ℕ} : (s.take n).length ≤ n := by
  induction n generalizing s with
  | zero => simp
  | succ m ih =>
    rw [take]
    cases s.destruct with
    | none => simp
    | some v =>
      obtain ⟨x, r⟩ := v
      simpa using ih

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