fastGrowing_def — Mathlib

English

If fundamentalSequence o = Sum.inl none, then fastGrowing o equals the successor function.

Русский

Если фундаментальная последовательность o равна Sum.inl none, то fastGrowing o равняется функции следующего.

LaTeX

$$$\\text{fastGrowing\\ o} = \\operatorname{succ}$$$

Lean4

theorem fastGrowing_def {o : ONote} {x} (e : fundamentalSequence o = x) :
    fastGrowing o =
      match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → FundamentalSequenceProp o x → ℕ → ℕ) x,
        e ▸ fundamentalSequence_has_prop o with
      | Sum.inl none, _ => Nat.succ
      | Sum.inl (some a), _ => fun i => (fastGrowing a)^[i] i
      | Sum.inr f, _ => fun i => fastGrowing (f i) i :=
  by
  subst x
  rw [fastGrowing]

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