noAtoms_withDensity

Mathlib.MeasureTheory.Measure.WithDensity

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

← MathLib Explorer

English

If μ has no atoms, then μ with density f also has no atoms for any density f.

Русский

Если у μ нет атомов, то μ с плотностью f также безатомна для любого f.

LaTeX

$$NoAtoms(μ_f)$$

Lean4

instance noAtoms_withDensity [NoAtoms μ] (f : α → ℝ≥0∞) : NoAtoms (μ.withDensity f) where
  measure_singleton _ := withDensity_absolutelyContinuous μ f (measure_singleton _)

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

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

Разделы

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

Аффилиация

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