English
For any ε > 0 and any countable index set, there exists a positive summable ε' with sum strictly less than ε in ENNReal.
Русский
Для любого ε > 0 и счётного множества индексов существует положительная сходящаяся сумма ε' с суммой меньше ε в 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) ∧ ∃ c, HasSum ε' c ∧ c < ε :=
by
cases nonempty_encodable ι
obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)
obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι
exact
⟨fun i ↦ ⟨ε' i, (hε' i).le⟩, fun i ↦ NNReal.coe_lt_coe.1 <| hε' i,
⟨c, hasSum_le (fun i ↦ (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩
