absolutelyContinuous_map

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

URI: https://scilib.ai/kg/mathlib#MeasurableEmbedding.absolutelyContinuous_map

English

If f is a measurable embedding and μ ≪ ν, then the push-forward μ.map f is absolutely continuous with respect to ν.map f.

Русский

Если f — измеримое вложение и μ ≪ ν, то μ.map f ≪ ν.map f.

LaTeX

$$hf.map f μ ≪ hf.map f ν$$

Lean4

theorem absolutelyContinuous_map (hf : MeasurableEmbedding f) (hμν : μ ≪ ν) : μ.map f ≪ ν.map f :=
  by
  intro t ht
  rw [hf.map_apply] at ht ⊢
  exact hμν ht

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

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

Разделы

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

Аффилиация

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