measurableSet_sigmaFiniteSetGE

Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

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

← MathLib Explorer

English

For any IsFiniteMeasure ν, the set μ.sigmaFiniteSetGE(ν, n) is measurable.

Русский

Для любой конечной меры ν множество μ.sigmaFiniteSetGE(ν, n) измеримо.

LaTeX

$$MeasurableSet(μ.sigmaFiniteSetGE ν n)$$

Lean4

theorem measurableSet_sigmaFiniteSetGE [IsFiniteMeasure ν] (n : ℕ) : MeasurableSet (μ.sigmaFiniteSetGE ν n) :=
  (exists_isSigmaFiniteSet_measure_ge μ ν n).choose_spec.1

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

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

Разделы

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

Аффилиация

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