Theorem Filter.Tendsto.limsup_comp_le_limsup

Modification history

2026-04-05 00:51
Mathlib/Order/LiminfLimsup.lean
feat(MeasureTheory): Fatou's lemma for countably generated filters (#37313)
Added Filter.Tendsto.limsup_comp_le_limsupView on Github →