Theorem MeasureTheory.Measure.forall_measure_inter_isCountablySpanning_eq_zero

Modification history

2026-03-18 19:14
Mathlib/MeasureTheory/Measure/Restrict.lean
feat(ProbabilityTheory): Conditional Jensen's Inequality (#27953) …
Added MeasureTheory.Measure.forall_measure_inter_isCountablySpanning_eq_zeroView on Github →