instSFiniteSumOfCountable — Mathlib

English

For Countable ι and a family m with each m(n) s-finite, the sum over m is s-finite.

Русский

Для счётного ι и семейства m с каждым n-м элементом s-finite, сумма над m также s-finite.

LaTeX

$$SFinite (Measure.sum m)$$

Lean4

instance [Countable ι] (m : ι → Measure α) [∀ n, SFinite (m n)] : SFinite (Measure.sum m) :=
  by
  change SFinite (Measure.sum (fun i ↦ m i))
  simp_rw [← sum_sfiniteSeq (m _), Measure.sum_sum]
  apply sfinite_sum_of_countable

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