extract_append_left' — Mathlib

English

If we form the concatenation a ++ b and then extract the interval [i, j], provided j ≤ size(a), the result equals the extraction of a on [i, j].

Русский

Если получить конкатенацию a ++ b, затем извлечь диапазон [i, j], и при этом j ≤ размер(a), то результат равен извлечению из a на [i, j].

LaTeX

$$$(a\;++\;b).extract\;i\;j = a.extract\;i\;j \quad (\,j \le a.size\,)$$$

Lean4

/-- This is a stronger version of `Array.extract_append_left`,
and should be upstreamed to replace that.
-/
theorem extract_append_left' {a b : Array α} {i j : Nat} (h : j ≤ a.size) : (a ++ b).extract i j = a.extract i j := by
  simp [h]

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