Theorems · Theorem · probability

ProbabilityTheory.Kernel.parallelComp_comp_parallelComp

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

Defined in

Mathlib.Probability.Kernel.Composition.KernelLemmas

Cited by

2 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel