condIndep' — Mathlib

English

If IsPiSystem p1 and p2 and hyp: CondIndepSets m' hm' p1 p2 μ, then CondIndep m' hm' (generateFrom p1) (generateFrom p2) μ.

Русский

Если p1 и p2 — Pi-системы и гипотеза 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 Ω)} (hp1m : ∀ s ∈ p1, MeasurableSet s) (hp2m : ∀ s ∈ p2, MeasurableSet s)
    (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2) (hyp : CondIndepSets m' hm' p1 p2 μ) :
    CondIndep m' (generateFrom p1) (generateFrom p2) hm' μ :=
  Kernel.IndepSets.indep' hp1m hp2m hp1 hp2 hyp

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