exists_pos_forall_sum_le — Mathlib

English

For a countable set s, there exists ε' with positive entries such that for every finite t ⊆ s, sum ε' over t ≤ ε.

Русский

Для счётного множества s существует ε' с положительными членами так, что для каждого конечного подмножества t ⊆ s сумма ε' по t не превышает ε.

LaTeX

$$$$\exists ε' : ι \to \mathbb{R}_{>0}, \; \forall t \text{ finite}, \; \sum_{i \in t} ε'_i \le ε.$$$$

Lean4

theorem exists_pos_forall_sum_le {ι : Type*} {s : Set ι} (hs : s.Countable) {ε : ℝ} (hε : 0 < ε) :
    ∃ ε' : ι → ℝ, (∀ i, 0 < ε' i) ∧ ∀ t : Finset ι, ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε := by
  classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le

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