English
For a countable set s, there exists a positive sequence ε' indexed by s with a HasSum bounded by ε.
Русский
Для счётного множества s существует положительная последовательность ε', индексированная по s, с HasSum не большей чем ε.
LaTeX
$$$$\exists ε' : s \to \mathbb{R}_{>0}, \ HasSum ε' c \land c \le ε.$$$$
Lean4
theorem exists_pos_hasSum_le {ι : Type*} {s : Set ι} (hs : s.Countable) {ε : ℝ} (hε : 0 < ε) :
∃ ε' : ι → ℝ, (∀ i, 0 < ε' i) ∧ ∃ c, HasSum (fun i : s ↦ ε' i) c ∧ c ≤ ε := by
classical
haveI := hs.toEncodable
rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
· conv_rhs => simp
split_ifs
exacts [hf0 _, zero_lt_one]
· simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]
