instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite

English

If each coordinate space has a locally finite measure and volume is locally finite, then the pi-measure is locally finite.

Русский

Если каждая координатная мера локально конечно измерима, то π-мерa также локально конечна.

LaTeX

$$$\\text{IsLocallyFiniteMeasure}(\\mathrm{pi}\\; \\mu)$$$

Lean4

instance {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, MeasureSpace (X i)]
    [∀ i, SigmaFinite (volume : Measure (X i))] [∀ i, IsLocallyFiniteMeasure (volume : Measure (X i))] :
    IsLocallyFiniteMeasure (volume : Measure (∀ i, X i)) :=
  pi.isLocallyFiniteMeasure

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