Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.is_bounded_bot

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.is_bounded_bot View on Github →