Theorems · Definition · probability

ProbabilityTheory.Kernel.IsCondKernel.casesOn

{α : Type u_1} →
  {β : Type u_2} →
    {Ω : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mΩ : MeasurableSpace Ω} →
            {κ : ProbabilityTheory.Kernel α (β × Ω)} →
              {κCond : ProbabilityTheory.Kernel (α × β) Ω} →
                {motive : κ.IsCondKernel κCond → Sort u} →
                  (t : κ.IsCondKernel κCond) → ((disintegrate : κ.fst.compProd κCond = κ) → motive ⋯) → motive t

Defined in

Mathlib.Probability.Kernel.Disintegration.Basic

Cited by

0 results in Mathlib

Foundations

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