takeD_left

Mathlib.Data.List.TakeDrop

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

← MathLib Explorer

English

TakeD (length l1) (l1 ++ l2) a = l1.

Русский

TakeD (длина l1) (l1 ++ l2) a = l1.

LaTeX

$$$\\mathrm{takeD}(\\mathrm{length}(l_1), (l_1 \\mathbin{+} l_2), a) = l_1$$$

Lean4

@[simp]
theorem takeD_left (l₁ l₂ : List α) (a : α) : takeD (length l₁) (l₁ ++ l₂) a = l₁ :=
  (takeD_eq_take a (by simp only [length_append, Nat.le_add_right])).trans take_left

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

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

Разделы

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

Аффилиация

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