tendsto_cofinite_zero_of_summable

English

If f: α → ℝ≥0 is summable, then f tends to 0 along the cofinite filter.

Русский

Если f: α → ℝ≥0 суммируема, то f стремится к 0 по фильтру cofinites.

LaTeX

$$Summable f → Tendsto f cofinite (nhds 0)$$

Lean4

theorem tendsto_cofinite_zero_of_summable {α} {f : α → ℝ≥0} (hf : Summable f) : Tendsto f cofinite (𝓝 0) :=
  by
  simp only [← summable_coe, ← tendsto_coe] at hf ⊢
  exact hf.tendsto_cofinite_zero

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