Selecting the point of an almost surely Dirac kernel

A kernel into a nonempty, countably generated measurable space that is Dirac almost everywhere for a given source measure agrees almost everywhere with the deterministic kernel of a measurable map. This is the measure-relative version of Mathlib's ProbabilityTheory.Kernel.IsDeterministic.exists_eq_deterministic, which assumes a deterministic kernel at every source point.

theorem ProbabilityTheory.Kernel.exists_ae_eq_deterministic_of_ae_exists_eq_dirac {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace.CountablyGenerated Y] [Nonempty Y] (κ : Kernel X Y) {μ : MeasureTheory.Measure X} (hκ : ∀ᵐ (x : X) ∂μ, ∃ (y : Y), κ x = MeasureTheory.Measure.dirac y) : ∃ (f : X → Y) (hf : Measurable f), ⇑κ =ᵐ[μ] ⇑(deterministic f hf)

If a kernel is almost everywhere a Dirac measure, then it agrees almost everywhere with the deterministic kernel of a measurable map.