Commit 2023-04-25 08:05 8f4f347b

View on Github →

chore: Generalise ess_sup lemmas (#3590) Match https://github.com/leanprover-community/mathlib/pull/18669

Estimated changes

Modified Mathlib/Order/Filter/ENNReal.lean

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

added theorem eventually_le_limsup

added theorem eventually_liminf_le

added theorem liminf_eq_top

added theorem limsup_eq_bot