finite_length_eq

Mathlib.Data.Set.Finite.List

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

English

The set of lists of fixed length n over a finite α is finite.

Русский

Множество списков фиксированной длины n над конечным α конечно.

LaTeX

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

Lean4

theorem finite_length_eq : {l : List α | l.length = n}.Finite :=
  List.Vector.finite

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

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

Разделы

Аффилиация

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