English
If b > 0 and the constant series with value b is summable over ι, then ι is finite.
Русский
Если b > 0 и константная последовательность b по ι суммируема, то множество индексов ι конечно.
LaTeX
$$0 < b \\\\land \\\\ Summable (fun _ : ι => b) \\\\Rightarrow \\\\ Finite ι$$
Lean4
theorem of_summable_const [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [Archimedean α]
[OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) : Finite ι :=
by
have H : ∀ s : Finset ι, #s • b ≤ ∑' _ : ι, b := fun s ↦ by simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum
obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb
have : ∀ s : Finset ι, #s ≤ n := fun s ↦ by simpa [nsmul_le_nsmul_iff_left hb] using (H s).trans hn
have : Fintype ι := fintypeOfFinsetCardLe n this
infer_instance
