indepFun_mul_right — Mathlib

English

A variant of IndepFun_mul_left with AE-measurability assumptions, preserving independence under multiplication.

Русский

Вариант IndepFun_mul_left₀ с AE-измеримостью, сохраняющий независимость при умножении.

LaTeX

$$$\IndepFun (f_i \cdot f_j) (f_k) κ μ$$$

Lean4

@[to_additive]
theorem indepFun_mul_right (hf_indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hij : i ≠ j)
    (hik : i ≠ k) : IndepFun (f i) (f j * f k) κ μ :=
  (hf_indep.indepFun_mul_left hf_meas _ _ _ hij.symm hik.symm).symm

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