default_eq

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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

English

The default instance equals the atomic partition.

Русский

По умолчанию экземпляр равен атомарному разбиению.

LaTeX

$$$\text{default} = \text{atomic}$$$

Lean4

@[simp]
theorem default_eq : (default : OrderedFinpartition n) = atomic n :=
  rfl

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

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

Разделы

Аффилиация

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