Theorem MeasureTheory.ae_restrict_le

Modification history

2025-01-14 09:42
Mathlib/MeasureTheory/Measure/Restrict.lean
chore: remove useless assumption in `ae_restrict_le` (#20732)
Modified MeasureTheory.ae_restrict_leView on Github →
2024-11-08 08:56
Mathlib/MeasureTheory/Measure/Restrict.lean
feat: relation between conditional measure and conditional kernel/expectation (#18697)
Added MeasureTheory.ae_restrict_leView on Github →