innerRegular_map_smul — 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 map of a left action is again inner regular. -/
@[to_additive /-- The image of a inner regular measure under map of a left additive action is again
    inner regular -/
    ]
instance innerRegular_map_smul {α} [Monoid α] [MulAction α G] [ContinuousConstSMul α G] [InnerRegular μ] (a : α) :
    InnerRegular (Measure.map (a • · : G → G) μ) :=
  InnerRegular.map_of_continuous (continuous_const_smul a)

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