harmonic_succ — Mathlib

English

The harmonic sequence satisfies a recurrence: harmonic(n+1) = harmonic(n) + 1/(n+1).

Русский

Гармоническая последовательность удовлетворяет рекуррентному закону: harmonic(n+1) = harmonic(n) + 1/(n+1).

LaTeX

$$$\operatorname{harmonic}(n+1) = \operatorname{harmonic}(n) + (n+1)^{-1}$$$

Lean4

@[simp]
theorem harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹ :=
  Finset.sum_range_succ ..

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