Theorems · Theorem · probability

ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id

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

Defined in: Mathlib.Probability.Kernel.Composition.KernelLemmas
Cited by: 0 results in Mathlib
Foundations: Depth 225 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: ProbabilityTheory.IsSFiniteKernel

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
ProbabilityTheory.IsSFiniteKernelstatement and proof · cited by 248
ProbabilityTheory.Kernel.compstatement and proof · cited by 129
ProbabilityTheory.Kernel.idstatement and proof · cited by 72
ProbabilityTheory.Kernel.parallelCompstatement and proof · cited by 49
ProbabilityTheory.Kernel.comp_idproof · cited by 8
ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelCompproof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.