mapₗ_ne_zero_iff

Mathlib.MeasureTheory.Measure.Map

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.mapₗ_ne_zero_iff

English

For measurable f, mapₗ f μ ≠ 0 iff μ ≠ 0.

Русский

Для измеримой f: mapₗ f μ ≠ 0 тогда и только тогда, когда μ ≠ 0.

LaTeX

$$$ mapₗ f μ \neq 0 \iff μ \neq 0 $ for measurable f$$

Lean4

theorem mapₗ_ne_zero_iff (hf : Measurable f) : Measure.mapₗ f μ ≠ 0 ↔ μ ≠ 0 :=
  (mapₗ_eq_zero_iff hf).not

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

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

Разделы

Аффилиация

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