Liminf lemmas (#16759)

Commit

3 years ago

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.

Author

RemyDegenne

Parents

2ce380c2

mathlib b2d70ba0 - feat(order/liminf_limsup): add limsup/liminf variants of some Limsup/Liminf lemmas (#16759)

mathlib
b2d70ba0 - feat(order/liminf_limsup): add limsup/liminf variants of some Limsup/Liminf lemmas (#16759)