fastGrowing_limit — Mathlib

English

If fundamentalSequence o = Sum.inr f, then fastGrowing o = fun i => fastGrowing (f i) i.

Русский

Если fundamentalSequence o = Sum.inr f, то fastGrowing o = функция i → fastGrowing (f(i)) i.

LaTeX

$$$\\forall o\\,{f}\\;\\big( \\text{fundamentalSequence } o = \\text{Sum.inr } f\\big) \\\\Rightarrow \\ operatorname{fastGrowing}(o) = \\lambda i. \\operatorname{fastGrowing}(f(i)) i$$$

Lean4

theorem fastGrowing_limit (o) {f} (h : fundamentalSequence o = Sum.inr f) :
    fastGrowing o = fun i => fastGrowing (f i) i := by rw [fastGrowing_def h]

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