Commit 2022-01-01 20:23 ebdbe6b0

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.