condIndepFun_iff_condIndepSet_preimage

English

Equivalence between iCondIndepFun and CondIndepSet_preimage under measurability assumptions on f and g.

Русский

Эквивалентность между iCondIndepFun и CondIndepSet_preimage при предположениях о измеримости функций f и g.

LaTeX

$$$\text{condIndepFun}_{m', hm'}(f,g,\mu) \iff \forall s,t, MeasurableSet(s) \to MeasurableSet(t) \to \text{CondIndepSet}_{m',hm'}(f^{-1}(s))(g^{-1}(t))\mu$$$

Lean4

theorem condIndepFun_iff_condIndepSet_preimage {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (hf : Measurable f)
    (hg : Measurable g) :
    CondIndepFun m' hm' f g μ ↔ ∀ s t, MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ :=
  by simp only [CondIndepFun, CondIndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

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