Theorems · Theorem · Lie groups

MeasureTheory.null_iff_of_isMulLeftInvariant

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] {s : Set G},
  IsOpen s → (μ s = 0 ↔ s = ∅ ∨ μ = 0)

Defined in: Mathlib.MeasureTheory.Group.Measure
Cited by: 1 results in Mathlib
Foundations: Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace TopologicalSpace BorelSpace Group IsTopologicalGroup MeasureTheory.Measure.IsMulLeftInvariant MeasureTheory.Measure.Regular

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement · cited by 9,879
Groupstatement and proof · cited by 6,238
IsOpenstatement and proof · cited by 2,400
BorelSpacestatement and proof · cited by 1,602
IsTopologicalGroupstatement and proof · cited by 469
MeasureTheory.Measure.IsMulLeftInvariantstatement and proof · cited by 118
MeasureTheory.Measure.Regularstatement and proof · cited by 61

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariantproof · cited by 1