Theorems · Theorem · probability

ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp

∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {mT : MeasurableSpace T} {κ : ProbabilityTheory.Kernel X Y} {X' : Type u_5}
  {mX' : MeasurableSpace X'} {η : ProbabilityTheory.Kernel X' Z} [ProbabilityTheory.IsSFiniteKernel η]
  {ξ : ProbabilityTheory.Kernel Z T} [ProbabilityTheory.IsSFiniteKernel ξ],
  (ξ.parallelComp ProbabilityTheory.Kernel.id).comp (η.parallelComp κ) = (ξ.comp η).parallelComp κ

Defined in

Mathlib.Probability.Kernel.Composition.KernelLemmas

Cited by

2 results in Mathlib

Foundations

Depth 227 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel