condIndep — Mathlib

English

If hp1m and hp2m give measurability for p1, p2, and hp1, hp2 are Pi-systems with hyp that CondIndepSets m' hm' p1 p2 μ, then CondIndep m' hm' (generateFrom p1) (generateFrom p2) μ.

Русский

Если даны условия на измеримость и Pi-системы p1, p2, и CondIndepSets m' hm' p1 p2 μ, то CondIndep между generateFrom(p1) и generateFrom(p2).

LaTeX

$$$\mathrm{CondIndep}(m', hm', \operatorname{generateFrom}(p_1), \operatorname{generateFrom}(p_2), \mu).$$$

Lean4

theorem condIndep {p1 p2 : Set (Set Ω)} (h1 : m₁ ≤ mΩ) (h2 : m₂ ≤ mΩ) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2)
    (hpm1 : m₁ = generateFrom p1) (hpm2 : m₂ = generateFrom p2) (hyp : CondIndepSets m' hm' p1 p2 μ) :
    CondIndep m' m₁ m₂ hm' μ :=
  Kernel.IndepSets.indep h1 h2 hp1 hp2 hpm1 hpm2 hyp

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