Zulip Chat Archive
Stream: mathlib4
Topic: Splitting MeasureTheory.Integral.Lebesgue.Basic
Jeremy Tan (Apr 13 2025 at 03:21):
After a preliminary PR to reduce imports I think I am happy with my split of MeasureTheory.Integral.Lebesgue.Basic at #23860.
But is there a better way? I don't know the answer
Jeremy Tan (Apr 13 2025 at 04:43):
Can ae_eq_of_ae_le_of_lintegral_le be proved without using monotone convergence?
Jeremy Tan (Apr 15 2025 at 02:39):
Merge conflict has been fixed and deprecated_module added
Last updated: May 02 2025 at 03:31 UTC