Commit 2025-01-14 09:42 a7b5e890

View on Github →

chore: remove useless assumption in ae_restrict_le (#20732)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

modified theorem MeasureTheory.ae_restrict_le

Modified Mathlib/Probability/Kernel/Condexp.lean