indep — Mathlib

English

Under pi-system hypotheses and measurability conditions, independence transfers from IndepSets p1 p2 μ to Indep (generateFrom p1) (generateFrom p2) μ.

Русский

При предположениях о пистеме и условиях измеримости независимость переносится из IndepSets p1 p2 μ в Indep(generateFrom p1, generateFrom p2; μ).

LaTeX

$$IsPiSystem p1 ∧ IsPiSystem p2 ∧ IndepSets p1 p2 μ ⇒ Indep(generateFrom p1, generateFrom p2; μ)$$

Lean4

theorem indep [IsZeroOrProbabilityMeasure μ] {p1 p2 : Set (Set Ω)} (h1 : m1 ≤ _mΩ) (h2 : m2 ≤ _mΩ) (hp1 : IsPiSystem p1)
    (hp2 : IsPiSystem p2) (hpm1 : m1 = generateFrom p1) (hpm2 : m2 = generateFrom p2) (hyp : IndepSets p1 p2 μ) :
    Indep m1 m2 μ :=
  Kernel.IndepSets.indep h1 h2 hp1 hp2 hpm1 hpm2 hyp

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