condIndepFun — Mathlib

English

If iCondIndepFun m' hm' f μ holds, then for any i ≠ j, CondIndepFun m' hm' (f_i) (f_j) μ holds.

Русский

Если iCondIndepFun m' hm' f μ, то для любых i ≠ j выполняется CondIndepFun m' hm' (f_i) (f_j) μ.

LaTeX

$$$\mathrm{CondIndepFun}(m', hm', f_i, f_j, \mu) \text{ for all } i \neq j.$$$

Lean4

theorem condIndepFun {β : ι → Type*} {m : ∀ x, MeasurableSpace (β x)} {f : ∀ i, Ω → β i}
    (hf_Indep : iCondIndepFun m' hm' f μ) {i j : ι} (hij : i ≠ j) : CondIndepFun m' hm' (f i) (f j) μ :=
  Kernel.iIndepFun.indepFun hf_Indep hij

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