mathlib

ba1cbfac - feat(topology/algebra/ordered/basic): Add alternative formulations of four lemmas. (#10630)

feat(topology/algebra/ordered/basic): Add alternative formulations of four lemmas. (#10630) Add alternative formulations of lemmas about interiors and frontiers of `Iic` and `Ici`. The existing formulations make typeclass assumptions `[no_top_order]` or `[no_bot_order]`. These alternative formulations assume instead that the endpoint of the interval is not top or bottom; and as such they can be applied in, e.g., `nnreal` and `ennreal`. Also, some lemmas now assume `(Ioi a).nonempty` or `(Iio a).nonempty` instead of `{b} (h : a < b)` or `{b} (h : b < a)`, respectively. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>