instInhabited

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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

English

Singleton-into-partitions: the atomic partition is the basic building block.

Русский

Атомарное разбиение на одиночные множества — базовый строительный блок.

LaTeX

$$$\text{atomic}(n):\text{OrderedFinpartition } n$ с частями размера 1$$

Lean4

instance : Inhabited (OrderedFinpartition n) :=
  ⟨atomic n⟩

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

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

Разделы

Аффилиация

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