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`.
