instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite

English

If each coordinate has an invariance under inversion, then the product measure on the Pi-space inherits the same invariance.

Русский

Если каждая координата инвариантна к обратному преобразованию, тогда произведение мер на Pi имеет ту же инвариантность.

LaTeX

$$$\\text{IsInvInvariant}(\\mathrm{pi}\\; μ)$$$

Lean4

@[to_additive]
instance {G : ι → Type*} [∀ i, Group (G i)] [∀ i, MeasureSpace (G i)] [∀ i, MeasurableMul (G i)]
    [∀ i, SigmaFinite (volume : Measure (G i))] [∀ i, IsMulRightInvariant (volume : Measure (G i))] :
    IsMulRightInvariant (volume : Measure (∀ i, G i)) :=
  pi.isMulRightInvariant _

Похожие утверждения