instSigmaFinite — Mathlib

English

A dual statement to 145611 with a countable index set for the second factor.

Русский

Дублирующее утверждение к 145611 для второй компоненты.

LaTeX

$$Eq (m.prod (Measure.sum m')) (Measure.sum (fun p => m.prod (m' p)))$$

Lean4

instance instSigmaFinite {α β : Type*} {_ : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {_ : MeasurableSpace β}
    {ν : Measure β} [SigmaFinite ν] : SigmaFinite (μ.prod ν) :=
  (μ.toFiniteSpanningSetsIn.prod ν.toFiniteSpanningSetsIn).sigmaFinite

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