comap_undef

Mathlib.MeasureTheory.Measure.Comap

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

English

If the injectivity condition fails, the comap is the zero measure.

Русский

Если инъективность не выполнена, comap — нулевая мера.

LaTeX

$$$\operatorname{comap}_l f μ = 0$$$

Lean4

theorem comap_undef {μ : Measure β} (h : ¬(Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ)) :
    comap f μ = 0 :=
  dif_neg h

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

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

Разделы

Аффилиация

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