fastGrowingε₀_two — Mathlib

English

The value of the ε₀-extended fast-growing sequence at 2 is 2048.

Русский

Значение расширенной до ε₀ быстрого роста в позиции 2 равно 2048.

LaTeX

$$$$ \operatorname{fastGrowing}_{\varepsilon_0}(2) = 2048. $$$$

Lean4

theorem fastGrowingε₀_two : fastGrowingε₀ 2 = 2048 := by
  norm_num [fastGrowingε₀, show oadd 0 1 0 = 1 from rfl, @fastGrowing_limit (oadd 1 1 0) _ rfl,
    show oadd 0 (2 : Nat).succPNat 0 = 3 from rfl, @fastGrowing_succ 3 2 rfl]

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