indepFun_mul_right₀ — Mathlib

English

An additive-corresponding form of IndepFun_mul_mul with AE-measurability for each f i.

Русский

Форма независимости, соответствующая аддитивной версии IndepFun_mul_mul с AE-измеримостью для каждого f_i.

LaTeX

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

Lean4

@[to_additive]
theorem indepFun_mul_right₀ (hf_indep : iIndepFun f κ μ) (hf_meas : ∀ i, AEMeasurable (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

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