@[reducible, inline]

abbrev ProbabilityTheory.IsTransitionProbability {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (κ : Kernel α β) : Prop

A transition probability from α to β is a function p : α × 𝓢_β → ℝ such that (1) for each x ∈ α, A ↦ p(x, A) is a probability measure on (β, 𝓢_β), and (2) for each A ∈ 𝓢_β, the map x ↦ p(x, A) is measurable. In Mathlib this is precisely an IsMarkovKernel.