of_summable_const — Mathlib

English

If b > 0 and the constant series with value b is summable, then Set.univ is finite.

Русский

Если b > 0 и константная сумма по единому индексу суммируема, то Set.univ конечно.

LaTeX

$$Set.univ.Finite$$

Lean4

theorem of_summable_const [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [Archimedean α]
    [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) : (Set.univ : Set ι).Finite :=
  finite_univ_iff.2 <| .of_summable_const hb hf

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