indepFun — Mathlib

English

If iIndepFun f μ holds for a family of functions f_i, then for any i ≠ j, f_i and f_j are independent with respect to μ.

Русский

Если выполняется iIndepFun f μ для семейства функций f_i, то для любых i ≠ j функции f_i и f_j независимы относительно μ.

LaTeX

$$iIndepFun f μ ⇒ ∀ i j, i ≠ j ⇒ IndepFun(f_i, f_j; μ)$$

Lean4

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

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