extract_eq_of_size_le_end — Mathlib

English

If a.size ≤ l, then extracting up to l from p yields the same as extracting up to a.size: a.extract p l = a.extract p a.size.

Русский

Если a.size ≤ l, то a.extract p l = a.extract p a.size.

LaTeX

$$$a.extract\;p\;l = a.extract\;p\;a.size \quad (a.size \le l)$$$

Lean4

theorem extract_eq_of_size_le_end {l p : Nat} {a : Array α} (h : a.size ≤ l) : a.extract p l = a.extract p a.size := by
  simp only [extract, Nat.min_eq_right h, Nat.sub_eq, Nat.min_self]

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