feat(topology/algebra/ordered): generalize two lemmas (#4177)
feat(topology/algebra/ordered): generalize two lemmas (#4177)

they hold for conditionally complete linear orders, not just for complete linear orders






leanprover-community/mathlib,leanprover-community/mathlib