Theorems · Theorem · probability

ProbabilityTheory.Kernel.Invariant.comp

∀ {α : Type u_1} {mα : MeasurableSpace α} {κ η : ProbabilityTheory.Kernel α α} {μ : MeasureTheory.Measure α},
  κ.Invariant μ → η.Invariant μ → (κ.comp η).Invariant μ

Defined in

Mathlib.Probability.Kernel.Invariance

Cited by

0 results in Mathlib

Foundations

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