Theorems · Theorem · measure theory

MeasureTheory.Content.is_add_left_invariant_innerContent

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : AddGroup G]
  [inst_2 : SeparatelyContinuousAdd G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) = μ K) →
    ∀ (g : G) (U : TopologicalSpace.Opens G),
      μ.innerContent ((TopologicalSpace.Opens.comap ↑(Homeomorph.addLeft g)) U) = μ.innerContent U

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupSeparatelyContinuousAdd