instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite

English

If each volume on X_i is Haar and Sigma-finite, the product volume on ∏ X_i is Haar.

Русский

Если каждая мера объема на X_i является Haar и сигма-конечна, то произведение объема на ∏ X_i также является Haar.

LaTeX

$$$\bigl(\forall i, IsHaarMeasure(volume_i)\bigr) \land \bigl(\forall i, SigmaFinite(volume_i)\bigr) \Rightarrow IsHaarMeasure(volume_{\prod i})$$$

Lean4

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

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