domSMul — Mathlib

English

For any DomMulAct g and a regular μ, the pushed-forward regular measure g • μ is regular.

Русский

Для любого действующего домножения g и регулярной μ мера g•μ регулярна.

LaTeX

$$$\\text{Regular}(g \\cdot \\mu)\\quad\\text{for all } g. $$$

Lean4

instance domSMul {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A] [MeasurableSpace A]
    [TopologicalSpace A] [BorelSpace A] [ContinuousConstSMul G A] {μ : Measure A} (g : Gᵈᵐᵃ) [Regular μ] :
    Regular (g • μ) :=
  .map <|
    .smul
      ((DomMulAct.mk.symm g : G)⁻¹)
        -- see Note [lower instance priority]

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