∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {mβ : (i : ι) → MeasurableSpace (β i)} {f g : (i : ι) → Ω → β i},
  (∀ (i : ι), f i =ᵐ[μ] g i) → ProbabilityTheory.iIndepFun f μ → ProbabilityTheory.iIndepFun g μ