Theorems · Theorem · measure theory

MeasureTheory.Measure.haar.prehaar_pos

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G},
  (interior U).Nonempty →
    ∀ {K : Set G} (h1K : IsCompact K),
      (interior K).Nonempty → 0 < MeasureTheory.Measure.haar.prehaar (↑K₀) U { carrier := K, isCompact' := h1K }

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceIsTopologicalGroup