instIsOpenPosMeasureForallVolumeOfSigmaFinite

English

If each component α_i carries a volume measure that is open-pos, then the product volume on ∏_i α_i is open-pos as well.

Русский

Если у каждого компонента α_i имеется меру объёма(volume) с открытым положительным свойством, то объёмная мера на произведении ∏_i α_i также имеет это свойство.

LaTeX

$$$\bigl(\forall i, IsOpenPosMeasure(volume\,:\, Measure(\alpha_i))\bigr) \Rightarrow IsOpenPosMeasure(volume:\, Measure(\forall i, \alpha_i))$$$

Lean4

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

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