Mathlib v3 is deprecated. Go to Mathlib v4

Theorem le_nhds_of_Limsup_eq_Liminf

Modification history

2021-05-14 14:25
src/topology/algebra/ordered/basic.lean
refactor(topology/algebra/ordered): reduce imports (#7601) …
Modified le_nhds_of_Limsup_eq_LiminfView on Github →
2018-04-25 13:06
analysis/topology/topological_structures.lean
feat(order): add liminf and limsup over filters (c.f. Sébastien Gouëzel's #115)
Added le_nhds_of_Limsup_eq_LiminfView on Github →