Theorems · Theorem · probability

ProbabilityTheory.Kernel.parallelComp_self_comp_copy

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsDeterministic κ],
  (κ.parallelComp κ).comp (ProbabilityTheory.Kernel.copy α) = (ProbabilityTheory.Kernel.copy β).comp κ

Defined in

Mathlib.Probability.Kernel.Deterministic

Cited by

2 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsDeterministic