le_map_apply_image

Mathlib.MeasureTheory.Measure.Map

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

← MathLib Explorer

English

For AEMeasurable f, μ(s) ≤ μ.map f (f''s) for any s.

Русский

Для AEMeasurable f, μ(s) ≤ μ.map f (f''s) для любого s.

LaTeX

$$$ \mu s \le \mu.map f (f'' s) $$$

Lean4

theorem le_map_apply_image {f : α → β} (hf : AEMeasurable f μ) (s : Set α) : μ s ≤ μ.map f (f '' s) :=
  (measure_mono (subset_preimage_image f s)).trans (le_map_apply hf _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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