Theorems · Theorem · probability

ProbabilityTheory.condDistrib.congr_simp

∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {x : MeasurableSpace α} [inst_3 : MeasurableSpace β] (Y Y_1 : α → Ω),
  Y = Y_1 →
    ∀ (X X_1 : α → β),
      X = X_1 →
        ∀ (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1) [inst_4 : MeasureTheory.IsFiniteMeasure μ],
          ProbabilityTheory.condDistrib Y X μ = ProbabilityTheory.condDistrib Y_1 X_1 μ_1

Defined in

Mathlib.Probability.Kernel.CondDistrib

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasurableSpaceMeasureTheory.IsFiniteMeasure