indepFun_div_div₀ — Mathlib

English

If f is iIndepFun, then for any finite disjoint S and T, the two finite subfamilies indexed by S and T are independent.

Русский

Если f является iIndepFun, то для любых конечных непересекающихся S и T две конечных подсемейства, индексируемые S и T, независимы.

LaTeX

$$$\text{IndepFun } (f i)_{i\in S} \;\perp\; (f i)_{i\in T} \; κ μ$$$

Lean4

@[to_additive]
theorem indepFun_div_div₀ (hf_indep : iIndepFun f κ μ) (hf_meas : ∀ i, AEMeasurable (f i) (κ ∘ₘ μ)) (i j k l : ι)
    (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : IndepFun (f i / f j) (f k / f l) κ μ :=
  (hf_indep.indepFun_prodMk_prodMk₀ hf_meas i j k l hik hil hjk hjl).comp measurable_div measurable_div

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