theorem ProbabilityTheory.cond_real_apply {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} (hms : MeasurableSet s) (μ : MeasureTheory.Measure Ω) (t : Set Ω) : μ[|s].real t = (μ.real s)⁻¹ * μ.real (s ∩ t)

The axiomatic definition of conditional probability derived from a measure-theoretic one.

theorem ProbabilityTheory.cond_isProbabilityMeasure_of_real {α : Type u_4} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hcs : μ.real s ≠ 0) : MeasureTheory.IsProbabilityMeasure μ[|s]

The conditional probability measure of any finite measure on any set of positive measure is a probability measure.