Theorems · Theorem · probability

ProbabilityTheory.Kernel.condKernel.congr_simp

∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
  [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ κ_1 : ProbabilityTheory.Kernel α (β × Ω)) (e_κ : κ = κ_1)
  [inst_2 : ProbabilityTheory.IsFiniteKernel κ], κ.condKernel = κ_1.condKernel

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsFiniteKernel