toFinite_absolutelyContinuous

Mathlib.MeasureTheory.Measure.WithDensityFinite

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

English

μ.toFinite ≪ μ (μ is absolutely continuous with respect to its finite version).

Русский

μ.toFinite ≪ μ (μ абсолютно непрерывна по отношению к своей конечной версии).

LaTeX

$$$ μ^{toFinite} \ll μ $$$

Lean4

theorem toFinite_absolutelyContinuous (μ : Measure α) [SFinite μ] : μ.toFinite ≪ μ :=
  Measure.ae_le_iff_absolutelyContinuous.mp ae_toFinite.le

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

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

Разделы

Аффилиация

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