mathlib

a779f6cf - feat(topology/algebra/ordered): convergent sequence is bounded above/below (#10424)

feat(topology/algebra/ordered): convergent sequence is bounded above/below (#10424) Also move lemmas `Ixx_mem_nhds` up to generalize them from `[linear_order α] [order_topology α]` to `[linear_order α] [order_closed_topology α]`.