English
If an iCondIndep relation holds for the index family m and sets s, then CondIndep holds between the left and each pair (m_i, m_j) with i ≠ j.
Русский
Если выполняется iCondIndepSets для семейства m и множеств s, то CondIndep справедлива между m' и любой пары m_i, m_j при i ≠ j.
LaTeX
$$$\mathrm{CondIndep}(m', (m_i), (m_j), hm', \mu) \text{ for all } i \neq j \text{ provided } \mathrm{iCondIndep}(m', hm', m, \mu).$$$
Lean4
theorem condIndep {m : ι → MeasurableSpace Ω} (h_indep : iCondIndep m' hm' m μ) {i j : ι} (hij : i ≠ j) :
CondIndep m' (m i) (m j) hm' μ :=
Kernel.iIndep.indep h_indep hij