Theorems · Definition · measure theory
MeasureTheory.Measure.haar.haarProduct
{G : Type u_1} → [Group G] → [inst : TopologicalSpace G] → Set G → Set (TopologicalSpace.Compacts G → ℝ)haarProduct K₀ is the product of intervals [0, (K : K₀)], for all compact sets K.
For all U, we can show that prehaar K₀ U ∈ haarProduct K₀.
- Defined in
- Mathlib.MeasureTheory.Measure.Haar.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- SetLike.coeproof · cited by 8,199
- Groupstatement and proof · cited by 6,238
- Set.univproof · cited by 3,945
- Set.Iccproof · cited by 1,702
- Set.piproof · cited by 405
- TopologicalSpace.Compactsstatement and proof · cited by 386
- MeasureTheory.Measure.haar.indexproof · cited by 20
Cited by4
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.haar.nonempty_iInter_clPrehaarstatement and proof · cited by 2
- MeasureTheory.Measure.haar.prehaar_mem_haarProductstatement · cited by 1
- MeasureTheory.Measure.haar.chaar_mem_haarProductstatement · cited by 1
- MeasureTheory.Measure.haar.mem_prehaar_emptystatement · cited by 0