inv_absolutelyContinuous

Mathlib.MeasureTheory.Group.Prod

URI: https://scilib.ai/kg/mathlib#MeasureTheory.inv_absolutelyContinuous

English

The inverse image measure μ.inv is absolutely continuous with respect to μ.

Русский

Обратная мера μ⁻¹ абсолютно непрерывна по отношению к μ.

LaTeX

$$$\mu^{\mathrm{inv}} \ll \mu$$$

Lean4

@[to_additive]
theorem inv_absolutelyContinuous : μ.inv ≪ μ :=
  (quasiMeasurePreserving_inv μ).absolutelyContinuous

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

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

Разделы

Аффилиация

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