mathlib

e7075b84 - chore(topology/algebra/ordered): fix assumptions in some lemmas (#3629)

chore(topology/algebra/ordered): fix assumptions in some lemmas (#3629) * Some `nhds_within_I??_eq_nhds_within_I??` lemmas assumed strict inequalities when this was not needed. * Remove TFAEs that only stated equality of three `nhds_within`s. Prove equality of `nhds_within`s instead. * Genralize `I??_mem_nhds_within_I??` to `order_closed_topology`.