Commit 2020-12-17 13:27 3685146a

chore(topology/algebra/ordered): deduplicate (#5399)

• Drop mem_nhds_unbounded in favor of mem_nhds_iff_exists_Ioo_subset'.
• Use (h : ∃ l, l < a) instead of {l} (hl : l < a) in mem_nhds_iff_exists_Ioo_subset'. This way we can apply the theorem without generating non-Prop goals and we can get the arguments directly from no_bot / no_top.
• add nhds_basis_Ioo' and nhds_basis_Ioo.