map_mono

Mathlib.MeasureTheory.Measure.Map

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

English

If μ ≤ ν and f is measurable, then μ.map f ≤ ν.map f.

Русский

Если μ ≤ ν и f измерима, то μ.map f ≤ ν.map f.

LaTeX

$$$ \mu \le \nu \Rightarrow (\mu.map f) \le (\nu.map f)$$$

Lean4

@[mono]
theorem map_mono {f : α → β} (h : μ ≤ ν) (hf : Measurable f) : μ.map f ≤ ν.map f :=
  le_iff.2 fun s hs ↦ by simp [hf.aemeasurable, hs, h _]

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

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

Разделы

Аффилиация

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