meas_iInter — Mathlib

English

For a finite index set i, if h : iIndepSets π κ μ and hs_i : ∀ i, i ∈ Finset.univ → f i ∈ π i, then almost surely κ a(⋂ i, f i) = ∏ i κ a(f i).

Русский

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

LaTeX

$$$ [Fintype\\ ι] (h : iIndepSets \\ π \\ κ \\ μ) (hs : ∀ i, i ∈ Finset.univ → f i ∈ π i) : \\forall^{{\\mathrm{ae}}} a \\partial μ, κ a (\\bigcap_i f i) = \\prod_i κ a (f i). $$$

Lean4

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

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