condIndepSet_of_mem — Mathlib

English

For iCondIndepSet with measurable s_n, and disjoint S, T, we have CondIndep m' generateFrom {s i} and generateFrom {t | ∃ j in S, s_j = t} etc.

Русский

Для iCondIndepSet со измеримыми s_n и несовместными S, T имеем CondIndep между generateFrom {s_i} и generateFrom {t | ∃ j в S, s_j = t} и т.д.

LaTeX

$$$\mathrm{CondIndep}(m', \operatorname{generateFrom}\{s_i\}, \operatorname{generateFrom}\{t \mid \exists j \le i, s_j = t\}, hm', \mu).$$$

Lean4

theorem condIndepSet_of_mem (hs : s ∈ S) (ht : t ∈ T) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t)
    (μ : Measure Ω) [IsFiniteMeasure μ] (h_indep : CondIndepSets m' hm' S T μ) : CondIndepSet m' hm' s t μ :=
  Kernel.IndepSets.indepSet_of_mem _ _ hs ht hs_meas ht_meas _ _ h_indep

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