harmonic_pos — Mathlib

English

For every natural number n ≥ 1, the harmonic number Hn is positive; equivalently, Hn > 0 when n ≠ 0.

Русский

Для любого натурального n ≥ 1 гармоническое число Hn положительно; эквивалентно тому, что Hn > 0, если n ≠ 0.

LaTeX

$$$H_n > 0 \quad\\text{for } n \\ge 1$$$

Lean4

theorem harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n :=
  by
  unfold harmonic
  rw [← Finset.nonempty_range_iff] at Hn
  positivity

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