condIndep — Mathlib

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

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