ae_mono

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

If μ ≤ ν as measures, then ae μ ≤ ae ν (preservation of almost everywhere relation under ≤).

Русский

Если μ ≤ ν, то ae μ ≤ ae ν.

LaTeX

$$μ ≤ ν → ae μ ≤ ae ν$$

Lean4

@[mono]
theorem ae_mono (h : μ ≤ ν) : ae μ ≤ ae ν :=
  h.absolutelyContinuous.ae_le

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

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

Разделы

Аффилиация

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