Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.liminf_le_limsup

Modification history

2021-11-02 10:26
src/order/liminf_limsup.lean
feat(topology/algebra/ordered/liminf_limsup): convergence of a sequence which does not oscillate infinitely (#10073) …
Modified filter.liminf_le_limsupView on Github →
2020-07-19 21:18
src/order/liminf_limsup.lean
refactor(order/filter/basic): add class `filter.ne_bot` (#3454) …
Modified filter.liminf_le_limsupView on Github →
2019-09-10 09:32
src/order/liminf_limsup.lean
chore(topology): sanity_check pass (#1416) …
Modified filter.liminf_le_limsupView on Github →
2019-06-14 17:40
src/order/liminf_limsup.lean
feat(measure_theory/integration): dominated convergence theorem (#1123) …
Added filter.liminf_le_limsupView on Github →