Theorem Filter.limsup_iInf_le_iInf_limsup

Modification history

2026-09-03 13:27

Mathlib/Order/LiminfLimsup.lean

chore(Order/liminfLimsup): use `to_dual` (#37757) …

Deleted Filter.limsup_iInf_le_iInf_limsup View on Github →

2026-04-03 13:23

Mathlib/Order/LiminfLimsup.lean

feat(Order/LiminfLimsup): add `iSup_liminf_le_liminf_iSup` (#37549) …

Added Filter.limsup_iInf_le_iInf_limsup View on Github →