isFiniteMeasure_sfiniteSeq

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

English

If μ is s-finite, then each term sfiniteSeq μ n is a finite measure.

Русский

Если μ является s-finite, то каждая мера sfiniteSeq μ n конечна.

LaTeX

$$IsFiniteMeasure (sfiniteSeq μ n)$$

Lean4

instance isFiniteMeasure_sfiniteSeq [h : SFinite μ] (n : ℕ) : IsFiniteMeasure (sfiniteSeq μ n) :=
  h.1.choose_spec.1 n

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

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

Разделы

Аффилиация

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