Commit 2020-01-02 09:04 ffa97852

feat(topology/algebra/ordered): prove that nhds_within (Ioi a) b ≠ ⊥ if a ≤ b (#1841)

• few similar statements Also drop decidability assumption in closure_Ioo etc. We don't care about using classical reasoning anyway, and usage of classical.DLO here doesn't lead to any noncomputable defs.