sum_sfiniteSeq

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.sum_sfiniteSeq

English

If ι is countable and m: ι → Measure α is such that each m(n) is finite, then the sum over m is s-finite.

Русский

Пусть ι счётно, и m: ι → Measure α так, что каждая m(n) конечна; тогда сумма m по индексу является s-finite.

LaTeX

$$SFinite (Measure.sum m)$$

Lean4

theorem sum_sfiniteSeq (μ : Measure α) [h : SFinite μ] : sum (sfiniteSeq μ) = μ :=
  h.1.choose_spec.2.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru