tsum_const_eq_top_of_ne_zero — Mathlib

English

If α is infinite and c ≠ 0, then ∑' α, c = ∞.

Русский

Если индексное множество бесконечно, и константа c ≠ 0, то ∑' α, c = ∞.

LaTeX

$$$\text{If } \alpha \text{ is infinite and } c \neq 0, \; \sum'_{\alpha} c = \infty$$$

Lean4

theorem tsum_const_eq_top_of_ne_zero {α : Type*} [Infinite α] {c : ℝ≥0∞} (hc : c ≠ 0) : ∑' _ : α, c = ∞ :=
  by
  have A : Tendsto (fun n : ℕ => (n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c)) :=
    by
    apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
    simp only [true_or, top_ne_zero, Ne, not_false_iff]
  have B : ∀ n : ℕ, (n : ℝ≥0∞) * c ≤ ∑' _ : α, c := fun n =>
    by
    rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
    simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s
  simpa [hc] using le_of_tendsto' A B

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