fastGrowing_one — Mathlib

English

The fast growing function at 1 reduces to a simple expression: fastGrowing 1 = fun n => 2 * n.

Русский

FastGrowing при 1 даёт простую формулу: fastGrowing 1 = fun n => 2 * n.

LaTeX

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

Lean4

@[simp]
theorem fastGrowing_one : fastGrowing 1 = fun n => 2 * n :=
  by
  rw [@fastGrowing_succ 1 0 rfl]; funext i; rw [two_mul, fastGrowing_zero]
  suffices ∀ a b, Nat.succ^[a] b = b + a from this _ _
  intro a b; induction a <;> simp [*, Function.iterate_succ', Nat.add_assoc, -Function.iterate_succ]

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