finite_length_le

Mathlib.Data.Set.Finite.List

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

English

For fixed n, the set of lists with length at most n is finite.

Русский

Для фиксированного n множество списков с длиной не более n конечно.

LaTeX

$$$\\{l : \\text{List } \\alpha \\mid \\text{length}(l) \\le n\\}.\\Finite$$$

Lean4

theorem finite_length_le : {l : List α | l.length ≤ n}.Finite := by
  simpa [Nat.lt_succ_iff] using finite_length_lt α (n + 1)

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

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

Разделы

Аффилиация

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