indepFun_div_right — Mathlib

English

A corollary form of IndepFun_div_left₀: independence of f_i from f_j / f_k is equivalent to the negation form on the other side.

Русский

Следствие IndepFun_div_left₀: независимость f_i от f_j / f_k равносильна противоположной форме с другой стороны.

LaTeX

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

Lean4

@[to_additive]
theorem indepFun_div_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_div_left hf_meas _ _ _ hij.symm hik.symm).symm

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