lt_top_of_tsum_ne_top — Mathlib

English

If ∑' i, a_i ≠ ∞, then each a_j < ∞ for every j.

Русский

Если сумма ∑' i, a_i не равна бесконечности, то каждый член a_j конечен.

LaTeX

$$$\left( \sum'_{i} a_i \neq \infty \right) \rightarrow a_j < \infty\; \text{for all } j$$$

Lean4

protected theorem lt_top_of_tsum_ne_top {a : α → ℝ≥0∞} (tsum_ne_top : ∑' i, a i ≠ ∞) (j : α) : a j < ∞ :=
  by
  contrapose! tsum_ne_top with h
  exact ENNReal.tsum_eq_top_of_eq_top ⟨j, top_unique h⟩

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