takeD_left'

Mathlib.Data.List.TakeDrop

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

English

If length(l1) = n, then takeD n (l1 ++ l2) a = l1.

Русский

Если длина l1 равна n, то takeD n (l1 ++ l2) a = l1.

LaTeX

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

Lean4

theorem takeD_left' {l₁ l₂ : List α} {n} {a} (h : length l₁ = n) : takeD n (l₁ ++ l₂) a = l₁ := by rw [← h];
  apply takeD_left

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

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

Разделы

Аффилиация

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