iCondIndepSets — Mathlib

English

If m' hm' are fixed and hs defines that each m_n = generateFrom(s_n) and iCondIndep m' hm' m μ holds, then iCondIndepSets m' hm' s μ holds.

Русский

Если для семейства m' hm' выполнено, что m_n = generateFrom(s_n) и iCondIndep m' hm' m μ, тогда iCondIndepSets m' hm' s μ.

LaTeX

$$$\mathrm{iCondIndepSets}(m', hm', s, \mu) \text{ given } \forall n, m_n = \operatorname{generateFrom}(s_n) \text{ and } iCondIndep(m', hm', m, \mu).$$$

Lean4

theorem iCondIndepSets {m : ι → MeasurableSpace Ω} {s : ι → Set (Set Ω)} (hms : ∀ n, m n = generateFrom (s n))
    (h_indep : iCondIndep m' hm' m μ) : iCondIndepSets m' hm' s μ :=
  Kernel.iIndep.iIndepSets hms h_indep

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