innerRegular_map_mul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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