Lemmas about composition of kernel #
theorem
ProbabilityTheory.Kernel.compProd_prodMkLeft_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(ξ : Kernel α β)
[IsSFiniteKernel ξ]
(κ : Kernel β γ)
[IsSFiniteKernel κ]
(a : α)
: