finite_length_lt

Mathlib.Data.Set.Finite.List

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

← MathLib Explorer

English

For a fixed n, the set of lists with length less than n is finite.

Русский

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

LaTeX

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

Lean4

theorem finite_length_lt : {l : List α | l.length < n}.Finite := by
  convert (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i; ext; simp

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

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

Разделы

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

Аффилиация

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