numBound_succ — Mathlib

English

For any k, D and n, numBound k D (n+1) equals numBound k D n times degBound k D n times D n.

Русский

Для любых k, D и n, numBound k D (n+1) равно numBound k D n умноженному на degBound k D n и на D n.

LaTeX

$$numBound\\,k\\,D\\,(n+1) = numBound\\,k\\,D\\,n \\cdot degBound\\,k\\,D\\,n \\cdot D\\,n$$

Lean4

@[simp]
theorem numBound_succ (k : ℕ) (D : ℕ → ℕ) (n) : numBound k D (n + 1) = numBound k D n * degBound k D n * D n := by
  rw [numBound]

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