meas_iInter — Mathlib

English

For a finite index set, if h : iIndepSets π κ μ and hs_i ∈ π i for all i, then κ a(⋂ i, s i) = ∏ i κ a(s i) almost surely.

Русский

Для конечного множества индексов, если h : iIndepSets π κ μ и для каждого i ∈ ι выполняется s i ∈ π i, то κ a(⋂ i s i) = ∏ i κ a(s i) почти surely.

LaTeX

$$$ [Fintype\\ ι] (h : iIndepSets π κ μ) (hs : \\forall i, s_i ∈ π i) : \\forall a, κ a (\\bigcap_i s_i) = \\prod_i κ a (s_i) \\; (\\ae\\ μ)$$$

Lean4

theorem meas_iInter [Fintype ι] (h : iIndep m κ μ) (hs : ∀ i, MeasurableSet[m i] (s i)) :
    ∀ᵐ a ∂μ, κ a (⋂ i, s i) = ∏ i, κ a (s i) :=
  by
  filter_upwards [h.meas_biInter (fun i (_ : i ∈ Finset.univ) ↦ hs _)] with a ha
  simp [← ha]

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