takeI_eq_take

Mathlib.Data.List.TakeDrop

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

← MathLib Explorer

English

If n ≤ length l, then takeI n l = take n l.

Русский

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

LaTeX

$$$\\forall n l,\\; n \\le |l| \\rightarrow \\mathrm{takeI}(n, l) = \\mathrm{take}(n, l)$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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