measurableSet_spanningSets

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

← MathLib Explorer

English

For σ-finite μ, each spanningSets μ i is a measurable set.

Русский

Для σ-конечной μ множество spanningSets μ i измеримо.

LaTeX

$$MeasurableSet (spanningSets μ i)$$

Lean4

theorem measurableSet_spanningSets (μ : Measure α) [SigmaFinite μ] (i : ℕ) : MeasurableSet (spanningSets μ i) :=
  MeasurableSet.iUnion fun j => MeasurableSet.iUnion fun _ => μ.toFiniteSpanningSetsIn.set_mem j

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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