absolutelyContinuous_of_le

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

The zero measure is absolutely continuous with respect to any μ.

Русский

Нулевая мера абсолютно непрерывна относительно любой меры μ.

LaTeX

$$$0 \ll \mu$$$

Lean4

theorem absolutelyContinuous_of_le (h : μ ≤ ν) : μ ≪ ν := fun s hs => nonpos_iff_eq_zero.1 <| hs ▸ le_iff'.1 h s

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

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

Разделы

Аффилиация

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