Theorems · Theorem · measure theory

MeasureTheory.measure_mul_measure_eq

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] [MeasurableInv G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant] (s t : Set G), ν' s ≠ 0 → ν' s ≠ ⊤ → μ' s * ν' t = ν' s * μ' t

Defined in

Mathlib.MeasureTheory.Group.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceGroupMeasurableMul₂MeasurableInvMeasureTheory.SigmaFiniteMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.Measure.IsMulLeftInvariant