Reciprocal_of_Null_Sequence

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

limits-of-sequencesnull-sequencesproofwiki

If x_n is a positive null sequence, then 1/x_n diverges to infinity.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic

theorem Reciprocal_of_Null_Sequence (x : ℕ → ℝ) (hpos : ∀ n, 0 < x n) (h : Filter.Tendsto x Filter.atTop (nhds 0)) : Filter.Tendsto (fun n => 1 / x n) Filter.atTop Filter.atTop := by sorry

Source

https://proofwiki.org/wiki/Reciprocal_of_Null_Sequence

View graph