mono_ac

Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

URI: https://scilib.ai/kg/mathlib#MeasureTheory.NullMeasurableSet.mono_ac

English

If s is null-measurable under μ and ν is absolutely continuous with respect to μ, then s is null-measurable under ν.

Русский

Если s нулево измеримо по μ и ν ≪ μ, то s нулево измеримо по ν.

LaTeX

$$NullMeasurableSet s ν$$

Lean4

theorem mono_ac (h : NullMeasurableSet s μ) (hle : ν ≪ μ) : NullMeasurableSet s ν :=
  h.preimage <| (QuasiMeasurePreserving.id μ).mono_left hle

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

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

Разделы

Аффилиация

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