indep_generateFrom_of_disjoint — Mathlib

English

If s is an iIndepSet with S,T disjoint, then the independent generation from S and T yields independence between the resulting sigma-algebras.

Русский

Если s — iIndepSet и S, T несовпадают, то независимое порождение из S и T даёт независимость полученных сигма-алгебр.

LaTeX

$$iIndepSet s μ → S T ⊆ ι → Disjoint S T → Indep(MeasurableSpace.generateFrom{t | ∃ n ∈ S, s n = t}, MeasurableSpace.generateFrom{t | ∃ k ∈ T, s k = t}, μ)$$

Lean4

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

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