fastGrowing_succ — Mathlib

English

If fundamentalSequence o = Sum.inl (some a), then fastGrowing o = fun i => (fastGrowing a)^[i] i.

Русский

Если fundamentalSequence o = Sum.inl (some a), то fastGrowing o = функция i → (fastGrowing a)^[i] i.

LaTeX

$$$\\forall o\\,{a}\\;\\big( \\text{fundamentalSequence } o = \\text{Sum.inl (some } a\\text{)} \\big) \\Rightarrow \\operatorname{fastGrowing}(o) = \\lambda i.(\\operatorname{fastGrowing}(a))^{[i]} i$$$

Lean4

theorem fastGrowing_succ (o) {a} (h : fundamentalSequence o = Sum.inl (some a)) :
    fastGrowing o = fun i => (fastGrowing a)^[i] i := by rw [fastGrowing_def h]

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