map_ne_zero_iff

Mathlib.MeasureTheory.Measure.Map

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

English

For AEMeasurable f μ, μ.map f ≠ 0 iff μ ≠ 0.

Русский

Для AEMeasurable f μ, μ.map f ≠ 0 тогда и только тогда когда μ ≠ 0.

LaTeX

$$$ \mathrm{map\_ne\_zero}\!:\; (\mathrm{AEMeasurable}(f, \mu)) \Rightarrow (\mu.map f \neq 0 \iff \mu \neq 0) $$$

Lean4

theorem map_ne_zero_iff (hf : AEMeasurable f μ) : μ.map f ≠ 0 ↔ μ ≠ 0 :=
  (map_eq_zero_iff hf).not

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

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

Разделы

Аффилиация

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