theorem ProbabilityTheory.IndepFun.measureReal_inter_preimage_eq_mul {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β} {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} (h : IndepFun f g μ) {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) : μ.real (f ⁻¹' s ∩ g ⁻¹' t) = μ.real (f ⁻¹' s) * μ.real (g ⁻¹' t)