indep' — Mathlib

English

With IsPiSystem and measurability hypotheses, independence of p1 and p2 implies independence of their generated sigma-algebras.

Русский

Имея предположения о пи-системах и измеримости, независимость p1 и p2 влечет независимость порожденных ими сигма-алгебр.

LaTeX

$$IsPiSystem(p1) ∧ IsPiSystem(p2) ∧ (∀ s ∈ p1, MeasurableSet s) ∧ (∀ s ∈ p2, MeasurableSet s) ∧ IndepSets p1 p2 μ ⇒ Indep(generateFrom p1, generateFrom p2; μ)$$

Lean4

theorem indep' [IsZeroOrProbabilityMeasure μ] {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) μ :=
  Kernel.IndepSets.indep' hp1m hp2m hp1 hp2 hyp

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