Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.eventually_lt_of_limsup_lt

Modification history

2020-03-16 20:04

src/order/liminf_limsup.lean

chore(order/liminf_limsup): lint and cleanup the file (#2162) …

Added filter.eventually_lt_of_limsup_lt View on Github →