Theorem Filter.Tendsto.liminf_le_liminf_comp

Modification history

2026-09-03 13:27
Mathlib/Order/LiminfLimsup.lean
chore(Order/liminfLimsup): use `to_dual` (#37757) …
Deleted Filter.Tendsto.liminf_le_liminf_compView on Github →
2026-04-05 00:51
Mathlib/Order/LiminfLimsup.lean
feat(MeasureTheory): Fatou's lemma for countably generated filters (#37313)
Added Filter.Tendsto.liminf_le_liminf_compView on Github →