∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  Measurable f →
    Measurable g →
      (ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
        MeasureTheory.Measure.map (fun ω => (ω, f ω, g ω)) μ =
          (μ.trim hm').bind
            ⇑(ProbabilityTheory.Kernel.id.prod
                (((ProbabilityTheory.condExpKernel μ m').map f).prod ((ProbabilityTheory.condExpKernel μ m').map g))))