not_summable_one_div_natCast

Mathlib.Analysis.PSeries

URI: https://scilib.ai/kg/mathlib#Real.not_summable_one_div_natCast

← MathLib Explorer

English

The harmonic series ∑_{n≥1} 1/n does not converge.

Русский

Гармонический ряд ∑_{n≥1} 1/n не сходится.

LaTeX

$$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n} \text{ diverges}.$$$$

Lean4

/-- Harmonic series is not unconditionally summable. -/
theorem not_summable_one_div_natCast : ¬Summable (fun n => 1 / n : ℕ → ℝ) := by
  simpa only [inv_eq_one_div] using not_summable_natCast_inv

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru