withDensity_of_ne_top'

Mathlib.MeasureTheory.Measure.WithDensity

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SigmaFinite.withDensity_of_ne_top'

← MathLib Explorer

English

If f is finite μ-a.e. (not infinite), then μ.withDensity f is sigma-finite.

Русский

Если f конечна μ-a.e., то μ.withDensity f сигма-конечна.

LaTeX

$$withDensity_of_ne_top'$$

Lean4

theorem withDensity_of_ne_top' [SigmaFinite μ] {f : α → ℝ≥0∞} (hf_ne_top : ∀ x, f x ≠ ∞) :
    SigmaFinite (μ.withDensity f) :=
  SigmaFinite.withDensity_of_ne_top <| ae_of_all _ hf_ne_top

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

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

Разделы

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

Аффилиация

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