theorem MeasureTheory.Measure.eq_prod_of_dirac_right (X : Type u_1) (Y : Type u_2) [MeasurableSpace X] [MeasurableSpace Y] (ν : Measure X) (y : Y) (μ : Measure (X × Y)) (marg_X : map Prod.fst μ = ν) (marg_Y : map Prod.snd μ = dirac y) : μ = ν.prod (dirac y)

theorem MeasureTheory.Measure.eq_prod_of_dirac_left (X : Type u_1) (Y : Type u_2) [MeasurableSpace X] [MeasurableSpace Y] (x : X) (ν : Measure Y) (μ : Measure (X × Y)) (marg_X : map Prod.fst μ = dirac x) (marg_Y : map Prod.snd μ = ν) : μ = (dirac x).prod ν