innerRegular_map_mul_right — Mathlib

English

The image of an inner regular measure under right multiplication is inner regular.

Русский

Образ при правом умножении сохраняет внутреннюю регулярность.

LaTeX

$$$ \text{InnerRegular}(\mu) \Rightarrow \text{InnerRegular}(\mathrm{map}(\cdot * g)(\mu)) $$$

Lean4

/-- The image of an inner regular measure under right multiplication is again inner regular. -/
@[to_additive /-- The image of an inner regular measure under right addition is again inner regular. -/
    ]
instance innerRegular_map_mul_right [IsTopologicalGroup G] [InnerRegular μ] (g : G) :
    InnerRegular (Measure.map (· * g) μ) :=
  InnerRegular.map_of_continuous (continuous_mul_right g)

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