Theorems · Theorem · probability

ProbabilityTheory.Kernel.parallelComp_comm

∀ {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}
  {η : ProbabilityTheory.Kernel Z T},
  (ProbabilityTheory.Kernel.id.parallelComp κ).comp (η.parallelComp ProbabilityTheory.Kernel.id) =
    (η.parallelComp ProbabilityTheory.Kernel.id).comp (ProbabilityTheory.Kernel.id.parallelComp κ)

Defined in

Mathlib.Probability.Kernel.Composition.KernelLemmas

Cited by

1 results in Mathlib

Foundations

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