is_mul_left_invariant_innerContent

English

If μ is invariant under left multiplication by any g in a group G (via K ↦ K.map (continuous_mul_left g)), then μ.innerContent is invariant under the corresponding Open comap under mulLeft.

Русский

Если μ инвариантно относительно левого умножения на любой элемент g группы G, то μ.innerContent инвариантно относительно соответствующего отображения Open по умножению слева.

LaTeX

$$∀g ∈ G, μ.innerContent (Opens.comap (Homeomorph.mulLeft g) U) = μ.innerContent U$$

Lean4

@[to_additive]
theorem is_mul_left_invariant_innerContent [Group G] [ContinuousMul G]
    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (g : G) (U : Opens G) :
    μ.innerContent (Opens.comap (Homeomorph.mulLeft g) U) = μ.innerContent U := by
  convert μ.innerContent_comap (Homeomorph.mulLeft g) (fun K => h g) U

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