feat(topology/algebra/ordered): new lemmas, update (#11184)
* In `exists_seq_strict_mono_tendsto'` and `exists_seq_strict_anti_tendsto'`, prove that `u n` belongs to the corresponding open interval.
* Add `exists_seq_strict_anti_strict_mono_tendsto`.
* Rename `is_lub_of_tendsto` to `is_lub_of_tendsto_at_top`, rename `is_glb_of_tendsto` to `is_glb_of_tendsto_at_bot`.
* Add `is_lub_of_tendsto_at_bot`, `is_glb_of_tendsto_at_top`.
