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]