Theorems · Definition · probability

ProbabilityTheory.Kernel.fst

{α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} → ProbabilityTheory.Kernel α (β × γ) → ProbabilityTheory.Kernel α β

Define a Kernel α β from a Kernel α (β × γ) by taking the map of the first projection. We use mapOfMeasurable for better defeqs.

Defined in

Mathlib.Probability.Kernel.Composition.MapComap

Cited by

81 results in Mathlib

Foundations

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