Theorems · Theorem · probability

ProbabilityTheory.Kernel.condKernelBorel.congr_simp

∀ {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] {mΩ : MeasurableSpace Ω} [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] (κ κ_1 : ProbabilityTheory.Kernel α (γ × Ω)) (e_κ : κ = κ_1)
  [inst_3 : ProbabilityTheory.IsFiniteKernel κ], κ.condKernelBorel = κ_1.condKernelBorel

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountablyGeneratedStandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernel