condIndep_generateFrom_of_disjoint

English

Let s be a family of sets with each s_n measurable. If hs is iCondIndepSet m' hm' s μ and S, T are disjoint, then CondIndep m' (generateFrom {t | ∃ n ∈ S, s_n = t}) (generateFrom {t | ∃ k ∈ T, s_k = t}) hm' μ.

Русский

Пусть s — семейство множеств с измеримыми s_n. Если hs является iCondIndepSet m' hm' s μ и S, T расходятся, то CondIndep между generateFrom множеств, порождаемых s на S и T, держится.

LaTeX

$$$\mathrm{CondIndep}(m', \operatorname{generateFrom}\{t \mid \exists n \in S, s_n = t\}, \operatorname{generateFrom}\{t \mid \exists k \in T, s_k = t\}, hm', \mu).$$$

Lean4

theorem condIndep_generateFrom_of_disjoint {s : ι → Set Ω} (hsm : ∀ n, MeasurableSet (s n))
    (hs : iCondIndepSet m' hm' s μ) (S T : Set ι) (hST : Disjoint S T) :
    CondIndep m' (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) hm' μ :=
  Kernel.iIndepSet.indep_generateFrom_of_disjoint hsm hs S T hST

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