exists_pos_sum_of_countable — Mathlib

English

For ENNReal there exists a positive summable ε' on a countable index with sum below ε.

Русский

Для ENNReal существует положительная сходящаяся последовательность ε' на счётном индексе с суммой меньше ε.

LaTeX

$$$$\exists ε' : ι \to \mathbb{R}_{>0}, \; HasSum ε' c \land c < ε.$$$$

Lean4

theorem exists_pos_sum_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [Countable ι] :
    ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ (∑' i, (ε' i : ℝ≥0∞)) < ε :=
  by
  rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩
  rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩
  rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩
  exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩

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