Theorems · Theorem · measure theory

MeasureTheory.Content.is_mul_left_invariant_outerMeasure

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [inst_2 : Group G]
  [inst_3 : SeparatelyContinuousMul G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) →
    ∀ (g : G) (A : Set G), μ.outerMeasure ((fun x => g * x) ⁻¹' A) = μ.outerMeasure A

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

0 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceR1SpaceGroupSeparatelyContinuousMul