W_succ — Mathlib

English

The recurrence for Wallis's product: W(k+1) = W(k) times the next Wallis factor.

Русский

Рекуррентное соотношение для произведения Уоллиса: W(k+1) = W(k) умножить на следующий фактор.

LaTeX

$$W(k+1) = W(k) \\cdot \\left( \\frac{2k+2}{2k+1} \\cdot \\frac{2k+2}{2k+3} \\right)$$

Lean4

theorem W_succ (k : ℕ) : W (k + 1) = W k * ((2 * k + 2) / (2 * k + 1) * ((2 * k + 2) / (2 * k + 3))) :=
  prod_range_succ _ _

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