iIndepSets — Mathlib

English

The same as indepFun but for a second formulation of iIndepFun.

Русский

То же самое для второй формулировки iIndepFun.

LaTeX

$$indepFun (hf_Indep : iIndepFun f κ μ) {i j} (hij : i ≠ j) : IndepFun (f i) (f j) κ μ$$

Lean4

theorem iIndepSets {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {m : ι → MeasurableSpace Ω}
    {s : ι → Set (Set Ω)} (hms : ∀ n, m n = generateFrom (s n)) (h_indep : iIndep m κ μ) : iIndepSets s κ μ :=
  fun S f hfs =>
  h_indep S fun x hxS => ((hms x).symm ▸ measurableSet_generateFrom (hfs x hxS) : MeasurableSet[m x] (f x))

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