condIndep_generateFrom_le_nat — Mathlib

English

If hs: 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' μ.

Русский

Если hs: iCondIndepSet m' hm' s μ и S, T расходятся, тогда CondIndep между generateFrom множества из s_n на 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_le_nat {s : ℕ → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iCondIndepSet m' hm' s μ)
    (n : ℕ) : CondIndep m' (generateFrom {s (n + 1)}) (generateFrom {t | ∃ k ≤ n, s k = t}) hm' μ :=
  Kernel.iIndepSet.indep_generateFrom_le_nat hsm hs n

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