Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-16 20:04 7a5496f6

View on Github →

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

chore(order/liminf_limsup): lint and cleanup the file, add some statements
use eventually_mono

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.eventually.congr

added theorem filter.eventually.congr_iff

Modified src/order/liminf_limsup.lean

modified theorem filter.Liminf_le_Limsup

modified theorem filter.Limsup_le_of_le

added theorem filter.eventually_lt_of_limsup_lt

added theorem filter.eventually_lt_of_lt_liminf

modified theorem filter.le_Liminf_of_le

added theorem filter.liminf_congr

added theorem filter.liminf_const

added theorem filter.limsup_congr

added theorem filter.limsup_const