Theorems · Theorem · probability

ProbabilityTheory.Kernel.parallelComp_id_left_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 ξ],
  (ProbabilityTheory.Kernel.id.parallelComp ξ).comp (κ.parallelComp η) = κ.parallelComp (ξ.comp η)

Defined in

Mathlib.Probability.Kernel.Composition.KernelLemmas

Cited by

5 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel