meas_iInter — Mathlib

English

If hf : iIndepFun f κ μ and hs : ∀ i, MeasurableSet[(mβ i).comap (f i)] (s i), then a.e. a: κ a(⋂ i, s i) = ∏ i κ a(s i).

Русский

Если hf : iIndepFun f κ μ и hs : ∀ i, MeasurableSet[(mβ i).comap (f i)] (s i), то почти для μ-мера κ a(⋂ i, s i) = ∏ i κ a(s i).

LaTeX

$$$ [Fintype\\ ι] (hf : iIndepFun f κ μ) (hs : \\forall i, MeasurableSet[(mβ i).comap (f i)] (s i)) : \\forall^{{\\mathrm{ae}}} a \\partial μ, κ a (\\bigcap_i s i) = \\prod_i κ a (s i) $$$

Lean4

theorem meas_iInter [Fintype ι] (hf : iIndepFun f κ μ) (hs : ∀ i, MeasurableSet[(mβ i).comap (f i)] (s i)) :
    ∀ᵐ a ∂μ, κ a (⋂ i, s i) = ∏ i, κ a (s i) :=
  hf.iIndep.meas_iInter hs

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