English
If two σ-algebras m1 and m2 are conditionally independent relative to m' and μ, then m2 and m1 are conditionally independent with the same conditioning: CondIndep m' m1 m2 hm' μ implies CondIndep m' m2 m1 hm' μ.
Русский
Если две σ-алгебры m1 и m2 условно независимы относительно m' и μ, то m2 и m1 тоже условно независимы при той же условной информации: CondIndep m' m1 m2 hm' μ → CondIndep m' m2 m1 hm' μ.
LaTeX
$$$\mathrm{CondIndep}(m', m_1, m_2, hm', \mu) \Rightarrow \mathrm{CondIndep}(m', m_2, m_1, hm', \mu)$$$
Lean4
@[symm]
theorem symm {m' m₁ m₂ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
{μ : Measure Ω} [IsFiniteMeasure μ] (h : CondIndep m' m₁ m₂ hm' μ) : CondIndep m' m₂ m₁ hm' μ :=
CondIndepSets.symm h
