mathlib
856cfd48 - feat(order/liminf_limsup): define `filter.blimsup`, `filter.bliminf` (#16819)

Commit

3 years ago

feat(order/liminf_limsup): define `filter.blimsup`, `filter.bliminf` (#16819) Also characterise `cofinite.limsup` and `cofinite.liminf` for the lattice of sets.

Author

ocfnash

Parents

8b80cafb

mathlib 856cfd48 - feat(order/liminf_limsup): define `filter.blimsup`, `filter.bliminf` (#16819)

mathlib
856cfd48 - feat(order/liminf_limsup): define `filter.blimsup`, `filter.bliminf` (#16819)