ae_map_le

Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

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

English

If g1 and g2 are equal μb-almost everywhere, then g1 ∘ f and g2 ∘ f are equal μa-almost everywhere.

Русский

Если g1 и g2 равны μb-почти везде, то g1 ∘ f и g2 ∘ f равны μa-почти везде.

LaTeX

$$g1 =ᵐ[μb] g2 → (g1 ∘ f) =ᵐ[μa] (g2 ∘ f)$$

Lean4

theorem ae_map_le (h : QuasiMeasurePreserving f μa μb) : ae (μa.map f) ≤ ae μb :=
  h.2.ae_le

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

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

Разделы

Аффилиация

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