Commit 2026-04-05 00:51 f47b6127

View on Github →

feat(MeasureTheory): Fatou's lemma for countably generated filters (#37313)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

modified theorem MeasureTheory.lintegral_liminf_le'

modified theorem MeasureTheory.lintegral_liminf_le

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.Tendsto.liminf_le_liminf_comp

added theorem Filter.Tendsto.limsup_comp_le_limsup