rdrop_append_length

Mathlib.Data.List.DropRight

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

← MathLib Explorer

English

Dropping length of l2 from l1 ++ l2 yields l1.

Русский

Удаление длины l2 из l1 ++ l2 дает l1.

LaTeX

$$$$ \mathrm{rdrop}(l_1 \;\; l_2).length = l_1. $$$$

Lean4

@[simp]
theorem rdrop_append_length {l₁ l₂ : List α} : List.rdrop (l₁ ++ l₂) (List.length l₂) = l₁ := by
  rw [rdrop_eq_reverse_drop_reverse, ← length_reverse, reverse_append, drop_left, reverse_reverse]

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

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

Разделы

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

Аффилиация

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