ascPochhammer_succ_left — Mathlib

English

The rising factorial satisfies a left recurrence: ascPochhammer S (n+1) = X · (ascPochhammer S n) ∘ (X+1).

Русский

У возрастания факториала существует левое вложение: ascPochhammer S (n+1) = X · (ascPochhammer S n) ∘ (X+1).

LaTeX

$$$ascPochhammer(S,n+1) = X \\cdot (ascPochhammer(S,n)) \\circ (X+1)$$$

Lean4

theorem ascPochhammer_succ_left (n : ℕ) : ascPochhammer S (n + 1) = X * (ascPochhammer S n).comp (X + 1) := by
  rw [ascPochhammer]

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