condIndep_of_condIndep_of_le_left

English

If CondIndep m' m1 m2 hm' μ holds and m3 ≤ m1, then CondIndep m' m3 m2 hm' μ also holds.

Русский

Если CondIndep m' m1 m2 hm' μ выполняется и m3 ≤ m1, то CondIndep m' m3 m2 hm' μ тоже выполняется.

LaTeX

$$$\mathrm{CondIndep}(m', m_3, m_2, hm', \mu) \text{ whenever } m_3 \le m_1 \text{ and } \mathrm{CondIndep}(m', m_1, m_2, hm', \mu).$$$

Lean4

theorem condIndep_of_condIndep_of_le_left {m' m₁ m₂ m₃ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω}
    [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] (h_indep : CondIndep m' m₁ m₂ hm' μ)
    (h31 : m₃ ≤ m₁) : CondIndep m' m₃ m₂ hm' μ :=
  Kernel.indep_of_indep_of_le_left h_indep h31

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