∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  [MeasureTheory.IsFiniteMeasure ρ], ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.const Unit ρ)