Theorems · Theorem · probability

ProbabilityTheory.Kernel.piecewise_apply

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] (a : α),
  (ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then κ a else η a

Defined in

Mathlib.Probability.Kernel.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidablePred