le_ae_restrict

Mathlib.MeasureTheory.Measure.Restrict

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

English

The almost-everywhere relation is monotone under restriction: the a.e. measure under μ|_s is less than or equal to that under μ.

Русский

Отношение almost-everywhere монотонно по ограничению: a.e. по μ|_s не превышает по μ.

LaTeX

$$$\ae (μ|_s) \leq \ae μ.$$$

Lean4

theorem le_ae_restrict : ae μ ⊓ 𝓟 s ≤ ae (μ.restrict s) := fun _s hs =>
  eventually_inf_principal.2 (ae_imp_of_ae_restrict hs)

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

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

Разделы

Аффилиация

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