Basic lemmas about Markov kernels

@[simp]

theorem ProbabilityTheory.Kernel.deterministic_inj {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.SeparatesPoints β] {f g : α → β} {hf : Measurable f} {hg : Measurable g} : deterministic f hf = deterministic g hg ↔ f = g

Two deterministic kernels are equal if and only if their underlying functions are equal.