condIndep_bot_left — Mathlib

English

For any σ-algebra m1, CondIndep m' ⊥ m1 hm' μ holds, i.e., the left σ-algebra m' is independent of the trivial σ-algebra on the right.

Русский

Для любой σ-алгебры m1 выполняется CondIndep m' ⊥ m1 hm' μ, т.е. левая σ-алгебра независима от тривиальной правой σ-алгебры.

LaTeX

$$$\mathrm{CondIndep}(m', \bot, m_1, hm', \mu)$$$

Lean4

theorem condIndep_bot_left (m₁ : MeasurableSpace Ω) {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω}
    [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] : CondIndep m' ⊥ m₁ hm' μ :=
  (Kernel.indep_bot_right m₁).symm

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