takeI_left

Mathlib.Data.List.TakeDrop

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

← MathLib Explorer

English

TakeI of the concatenation l1 ++ l2 with index length l1 equals l1.

Русский

TakeI длины списка l1 из конкатенации l1 ++ l2 даёт l1.

LaTeX

$$$\\mathrm{takeI}(|l_1|, l_1 \\mathbin{+} l_2) = l_1$$$

Lean4

@[simp]
theorem takeI_left (l₁ l₂ : List α) : takeI (length l₁) (l₁ ++ l₂) = l₁ :=
  (takeI_eq_take (by simp only [length_append, Nat.le_add_right])).trans take_left

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

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

Разделы

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

Аффилиация

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