Theorems · Theorem · measure theory

MeasureTheory.Content.innerContent_pos_of_is_mul_left_invariant

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : Group G]
  [inst_2 : IsTopologicalGroup G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) →
    ∀ (K : TopologicalSpace.Compacts G),
      μ K ≠ 0 → ∀ (U : TopologicalSpace.Opens G), (↑U).Nonempty → 0 < μ.innerContent U

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroup