rdrop_append_length_add

Mathlib.Data.List.DropRight

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

← MathLib Explorer

English

Dropping (length l2 + k) from l1 ++ l2 equals dropping k from l1.

Русский

Удаление длины (|l2| + k) из l1 ++ l2 даёт удаление k из l1.

LaTeX

$$$$ \mathrm{rdrop}(l_1 ++ l_2)\, (|l_2| + k) = \mathrm{rdrop}(l_1)\, k. $$$$

Lean4

@[simp]
theorem rdrop_append_length_add {l₁ l₂ : List α} (k : ℕ) : List.rdrop (l₁ ++ l₂) (length l₂ + k) = List.rdrop l₁ k := by
  rw [← rdrop_add, rdrop_append_length]

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

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

Разделы

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

Аффилиация

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