Theorems · Theorem · Lie groups

MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [h : μ.InnerRegularCompactLTTop],
  μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ μ s ≠ ⊤

Defined in

Mathlib.MeasureTheory.Group.Measure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceBorelSpaceGroupIsTopologicalGroupMeasureTheory.Measure.InnerRegularCompactLTTop