condIndep_bot_right — Mathlib

English

For any σ-algebra m1, CondIndep m' m1 ⊥ hm' μ holds, meaning m' is conditionally independent of the trivial (bottom) σ-algebra on Ω.

Русский

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

LaTeX

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

Lean4

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

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