Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.Liminf_le_Liminf_of_le

Modification history

2018-04-25 13:06

order/liminf_limsup.lean

feat(order): add liminf and limsup over filters (c.f. Sébastien Gouëzel's #115)

Added filter.Liminf_le_Liminf_of_le View on Github →