indepFun_mul_left — Mathlib

English

If f is iIndepFun and each f i is measurable, then for i ≠ k and j ≠ k, the product f i · f j is independent of f k.

Русский

Если f образует i-независимую совокупность и каждый f_i измерим, то произведение f_i · f_j независимо от f_k при i ≠ k, j ≠ k.

LaTeX

$$$ \\operatorname{iIndepFun} f μ \\rightarrow (\\forall i, Measurable (f i)) \\rightarrow \\forall i j k, i \\neq k \\rightarrow j \\neq k \\rightarrow \\operatorname{IndepFun} (f i * f j) (f k) μ$$$

Lean4

@[to_additive]
theorem indepFun_mul_left (hf_indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k)
    (hjk : j ≠ k) : IndepFun (f i * f j) (f k) μ :=
  Kernel.iIndepFun.indepFun_mul_left hf_indep hf_meas i j k hik hjk

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