takeI_left'

Mathlib.Data.List.TakeDrop

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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