indep' — Mathlib

English

Reiterates that Indep' translates independence from pi-systems to their generated sigma-algebras.

Русский

Повторяет перевод независимости пи-систем в независимость порожденных сигма-алгебр.

LaTeX

$$indep'(hp1m,hp2m,hp1,hp2,hyp) : Indep( generateFrom p1, generateFrom p2, κ, μ )$$

Lean4

theorem indep' {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ] {p1 p2 : Set (Set Ω)}
    (hp1m : ∀ s ∈ p1, MeasurableSet s) (hp2m : ∀ s ∈ p2, MeasurableSet s) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2)
    (hyp : IndepSets p1 p2 κ μ) : Indep (generateFrom p1) (generateFrom p2) κ μ :=
  hyp.indep (generateFrom_le hp1m) (generateFrom_le hp2m) hp1 hp2 rfl rfl

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