instFintype

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

URI: https://scilib.ai/kg/mathlib#OrderedFinpartition.instFintype

English

The type of ordered finite partitions of n is finite; i.e., OrderedFinpartition(n) has finitely many elements.

Русский

Тип упорядоченных фин-разделов числа n конечен; то есть у OrderedFinpartition(n) счетное число элементов.

LaTeX

$$$\\#\\mathrm{OrderedFinpartition}(n) < \\infty$$$

Lean4

noncomputable instance : Fintype (OrderedFinpartition n) :=
  Fintype.ofInjective _ (injective_embSigma n)

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

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

Разделы

Аффилиация

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