extract_eq_nil_of_start_eq_end

Mathlib.Data.Array.Extract

URI: https://scilib.ai/kg/mathlib#Array.extract_eq_nil_of_start_eq_end

← MathLib Explorer

English

For any array a and any index i, extracting the subarray from i to i yields the empty array.

Русский

Для любого массива a и любого индекса i извлечение подмассива от i до i даёт пустой массив.

LaTeX

$$$a.extract\;i\;i = \#[]$$$

Lean4

@[simp]
theorem extract_eq_nil_of_start_eq_end {a : Array α} : a.extract i i = #[] :=
  by
  refine extract_empty_of_stop_le_start ?h
  exact Nat.le_refl i

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru