condIndep_of_condIndep_of_le_right

English

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

Русский

Если CondIndep m' m1 m2 hm' μ, и m3 ≤ m2, то CondIndep m' m1 m3 hm' μ также верно.

LaTeX

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

Lean4

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

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