exists_pos_sum_of_countable' — Mathlib

English

Let ε > 0 and I be a-countable. Then there exists a function ε' : I → ℝ≥0∞ such that each ε'(i) > 0 and the (extended) sum ∑' i, ε'(i) is strictly less than ε.

Русский

Пусть ε > 0 и множество индексов I счётно. Существует функция ε' : I → ℝ≥0∞ такая, что для каждого i выполняется ε'(i) > 0, и нерасширяемая сумма ∑' i ε'(i) < ε.

LaTeX

$$$\\\\exists ε' : ι → ℝ_{\\\\ge 0}^{∞}, (∀ i, 0 < ε'(i)) \\\\land \\\\sum' i, ε'(i) < ε$$$

Lean4

theorem exists_pos_sum_of_countable' {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [Countable ι] :
    ∃ ε' : ι → ℝ≥0∞, (∀ i, 0 < ε' i) ∧ ∑' i, ε' i < ε :=
  let ⟨δ, δpos, hδ⟩ := exists_pos_sum_of_countable hε ι
  ⟨fun i ↦ δ i, fun i ↦ ENNReal.coe_pos.2 (δpos i), hδ⟩

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