Theorems · Theorem · probability

ProbabilityTheory.Kernel.piecewise.congr_simp

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s s_1 : Set α} (e_s : s = s_1)
  {inst : DecidablePred fun x => x ∈ s} [inst_1 : DecidablePred fun x => x ∈ s_1] (hs : MeasurableSet s)
  (κ κ_1 : ProbabilityTheory.Kernel α β),
  κ = κ_1 →
    ∀ (η η_1 : ProbabilityTheory.Kernel α β),
      η = η_1 → ProbabilityTheory.Kernel.piecewise hs κ η = ProbabilityTheory.Kernel.piecewise ⋯ κ_1 η_1

Defined in

Mathlib.Probability.Kernel.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidablePred