map_smul

Mathlib.MeasureTheory.Group.Action

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

English

The pushforward by a smul map is invariant under the original action: map (c • ·) μ = μ.

Русский

Образующая по смул-отображению инвариантна относительно исходного действия: map (c • ·) μ = μ.

LaTeX

$$$\\operatorname{map}(c\\cdot,\\mu) = \\mu$$$

Lean4

@[to_additive (attr := simp)]
protected theorem map_smul : map (c • ·) μ = μ :=
  (measurePreserving_smul c μ).map_eq

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

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

Разделы

Аффилиация

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