is_mul_left_invariant_outerMeasure

English

For a group G with continuous multiplication, if μ(K.map(·, continuous_mul_left g)) = μ(K) for all compact K and g, then μ.outerMeasure((g^{-1}•)^{-1}(A)) = μ.outerMeasure(A) for all A.

Русский

Для группы G с непрерывным умножением, если μ(K.map f) = μ(K) для всех компактных K и для каждого g, тогда μ.outerMeasure(g^{-1}A) = μ.outerMeasure(A).

LaTeX

$$$$μ.outerMeasure((g\\cdot)^{-1}A) = μ.outerMeasure(A)\\quad\\text{for all }g\\in G.$$$

Lean4

@[to_additive]
theorem is_mul_left_invariant_outerMeasure [Group G] [ContinuousMul G]
    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (g : G) (A : Set G) :
    μ.outerMeasure ((g * ·) ⁻¹' A) = μ.outerMeasure A := by
  convert μ.outerMeasure_preimage (Homeomorph.mulLeft g) (fun K => h g) A

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