indep_generateFrom_le — Mathlib

English

If m is antitone and indep relations hold, then the supremum is independent with respect to μ.

Русский

Если m антотонно убывает и независимость сохраняется, то супремум независим относительно μ.

LaTeX

$$Indep(iSup_i m_i, m1; μ) при Antitone(m)$$

Lean4

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

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