tendsto_eulerMascheroniSeq — Mathlib

English

The Euler–Mascheroni sequence converges to γ: lim eulerMascheroniSeq(n) = γ.

Русский

Последовательность Эйлера–Машчерони сходится к γ: lim eulerMascheroniSeq(n) = γ.

LaTeX

$$\lim_{n\to\infty} eulerMascheroniSeq(n) = \gamma$$

Lean4

theorem tendsto_eulerMascheroniSeq : Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant) :=
  by
  have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_
  · rwa [eulerMascheroniConstant, this.limUnder_eq]
  · exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩

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