length_dropSlice

Mathlib.Data.List.TakeDrop

URI: https://scilib.ai/kg/mathlib#List.length_dropSlice

← MathLib Explorer

English

If i < |xs| and j > 0, then |dropSlice i j xs| < |xs|.

Русский

Если i < |xs| и j > 0, то |dropSlice i j xs| < |xs|.

LaTeX

$$$0 < j \\Rightarrow i < |xs| \\Rightarrow |\\mathrm{dropSlice}(i,j,xs)| < |xs|$$$

Lean4

@[simp, grind =]
theorem length_dropSlice (i j : ℕ) (xs : List α) : (dropSlice i j xs).length = xs.length - min j (xs.length - i) := by
  induction xs generalizing i j with cases i with grind [dropSlice]

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

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

Разделы

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

Аффилиация

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