rdrop_add

Mathlib.Data.List.DropRight

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

English

Dropping i elements from l and then dropping j elements yields dropping i + j elements from l.

Русский

Удаление i элементов из списка, затем j элементов, равно удалению i + j элементов.

LaTeX

$$$$ (l.rdrop i).rdrop j = l.rdrop (i + j). $$$$

Lean4

theorem rdrop_add (i j : ℕ) : (l.rdrop i).rdrop j = l.rdrop (i + j) := by
  simp_rw [rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop]

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

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

Разделы

Аффилиация

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