takeD_eq_take

Mathlib.Data.List.TakeDrop

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

← MathLib Explorer

English

If n ≤ length l, then takeD n l a = take n l.

Русский

Если n ≤ |l|, то takeD n l a = take n l.

LaTeX

$$$\\forall {n} {l} {a},\\; n \\le |l| \\rightarrow \\mathrm{takeD}\\, n\\, l\\, a = \\mathrm{take}\\, n\\, l$$$

Lean4

theorem takeD_eq_take : ∀ {n} {l : List α} a, n ≤ length l → takeD n l a = take n l
  | 0, _, _, _ => rfl
  | _ + 1, _ :: _, a, h => congr_arg (cons _) <| takeD_eq_take a <| le_of_succ_le_succ h

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

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

Разделы

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

Аффилиация

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