theorem
ProbabilityTheory.Kernel.parallelComp_apply_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
{η : Kernel γ δ}
{x : α × γ}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
(s : Set β)
(t : Set δ)
:
theorem
ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{f : α → γ}
{g : β → δ}
(hf : Measurable f)
(hg : Measurable g)
: