measure_compl_sigmaFiniteSet

Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

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

← MathLib Explorer

English

A measure μ is sigma-finite iff μ(μ.sigmaFiniteSetᶜ) = 0.

Русский

Мера μ сигма-финитна тогда и только тогда, когда μ(μ.sigmaFiniteSetᶜ) = 0.

LaTeX

$$$$\mu(\mu.sigmaFiniteSet^c) = 0 \iff \SigmaFinite(μ).$$$$

Lean4

@[simp]
theorem measure_compl_sigmaFiniteSet (μ : Measure α) [SigmaFinite μ] : μ μ.sigmaFiniteSetᶜ = 0 :=
  measure_compl_sigmaFiniteSetWRT Measure.AbsolutelyContinuous.rfl

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

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

Разделы

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

Аффилиация

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