indep_generateFrom_lt — Mathlib

English

If m is monotone and indep relations hold at each index, then the supremum over all indices is independent of m1.

Русский

Если m монотонно возрастает и при каждом индексе соблюдается независимость, то супремум по всем индексам независим от m1.

LaTeX

$$Indep(iSup_i m_i, m1; μ)$$

Lean4

theorem indep_generateFrom_lt [Preorder ι] {s : ι → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s μ)
    (i : ι) : Indep (generateFrom {s i}) (generateFrom {t | ∃ j < i, s j = t}) μ :=
  Kernel.iIndepSet.indep_generateFrom_lt hsm hs i

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