fastGrowing_two

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.fastGrowing_two

English

For the special case o = 2, fastGrowing 2 equals the function n ↦ (2^n) · n.

Русский

Для случая o = 2, fastGrowing 2 равняется функции n ↦ (2^n) · n.

LaTeX

$$$\\operatorname{fastGrowing}(2) = \\lambda n. (2^{n}) \\cdot n$$$

Lean4

@[simp]
theorem fastGrowing_two : fastGrowing 2 = fun n => (2 ^ n) * n :=
  by
  rw [@fastGrowing_succ 2 1 rfl]
  simp

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

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

Разделы

Аффилиация

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