takeI_nil

Mathlib.Data.List.TakeDrop

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

English

For any n, takeI n of the empty list equals the replication of default n times.

Русский

Для любого n takeI n пустого списка равно replicate n default.

LaTeX

$$$\\mathrm{takeI}(n, \\emptyset) = \\mathrm{replicate}(n, \\mathrm{default})$$$

Lean4

@[simp]
theorem takeI_nil : ∀ n, takeI n (@nil α) = replicate n default
  | 0 => rfl
  | _ + 1 => congr_arg (cons _) (takeI_nil _)

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

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

Разделы

Аффилиация

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