absolutelyContinuous_restrict

Mathlib.MeasureTheory.Measure.Restrict

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.absolutelyContinuous_restrict

English

The restricted measure μ|s is absolutely continuous with respect to μ.

Русский

Ограниченная мера μ|s абсолютно непрерывна по отношению к μ.

LaTeX

$$$(\mu|s) \ll \mu.$$$

Lean4

theorem absolutelyContinuous_restrict : μ.restrict s ≪ μ :=
  Measure.absolutelyContinuous_of_le Measure.restrict_le_self

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

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

Разделы

Аффилиация

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