instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite

English

There is a corresponding instance asserting invariance for the product volume under inversion when the coordinate volumes are invariant.

Русский

Существует инстанс инвариантности для произведения объема при инверсии, если координатные объемы инвариантны.

LaTeX

$$$\\text{IsInvInvariant}(\\mathrm{volume})$$$

Lean4

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

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