Theorems · Theorem · Lie groups

MeasureTheory.Measure.measure_inv

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G)
  [μ.IsInvInvariant] (A : Set G), μ A⁻¹ = μ A

Defined in

Mathlib.MeasureTheory.Group.Measure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceInvolutiveInvMeasurableInvMeasureTheory.Measure.IsInvInvariant