map_of_not_aemeasurable

Mathlib.MeasureTheory.Measure.Map

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

English

If f is not AEMeasurable with respect to μ, then μ.map f = 0.

Русский

Если f не является а.е.-измеримой относительно μ, то μ.map f = 0.

LaTeX

$$$ \neg \mathrm{AEMeasurable}(f, \mu) \Rightarrow \mu.map f = 0 $$$

Lean4

@[simp]
theorem map_of_not_aemeasurable {f : α → β} {μ : Measure α} (hf : ¬AEMeasurable f μ) : μ.map f = 0 := by simp [map, hf]

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

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

Разделы

Аффилиация

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