meas_biInter — Mathlib

English

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

Русский

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

LaTeX

$$$ (hf : iIndepFun f κ μ) \\Rightarrow (hs : \\forall i, i \\in S \\Rightarrow MeasurableSet[(mβ i).comap (f i)] (s i)) \Rightarrow \\forall a, κ a (\\bigcap_{i \\in S} s i) = \\prod_{i \\in S} κ a (s i) $$$

Lean4

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

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