map

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\mu \ll \nu \rightarrow \mathrm{Measurable}(f) \rightarrow (\mathrm{map}\, f\, \mu) \ll (\mathrm{map}\, f\, \nu)$$$

Lean4

@[mono]
protected theorem map (h : μ ≪ ν) {f : α → β} (hf : Measurable f) : μ.map f ≪ ν.map f :=
  AbsolutelyContinuous.mk fun s hs => by simpa [hf, hs] using @h _

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

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

Разделы

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

Аффилиация

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