Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-02 21:39 b2d70ba0

View on Github →

feat(order/liminf_limsup): add limsup/liminf variants of some Limsup/Liminf lemmas (#16759) Also make sure that similar lemmas follow each other in the order Limsup, Liminf, limsup, liminf.

Estimated changes