sfiniteSeq_le

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

English

For μ s-finite, every term of the sequence is dominated by μ: sfiniteSeq μ n ≤ μ.

Русский

Для μ, являющейся s-finite, каждый член последовательности не превосходит μ: sfiniteSeq μ n ≤ μ.

LaTeX

$$sfiniteSeq μ n ≤ μ$$

Lean4

theorem sfiniteSeq_le (μ : Measure α) [SFinite μ] (n : ℕ) : sfiniteSeq μ n ≤ μ :=
  (le_sum _ n).trans (sum_sfiniteSeq μ).le

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

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

Разделы

Аффилиация

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