mathlib

ac2e9dbf - feat(data/real/{e,}nnreal): add some order isomorphisms (#14900)

feat(data/real/{e,}nnreal): add some order isomorphisms (#14900) * If `a` is a nonnegative real number, then - `set.Icc (0 : ℝ) (a : ℝ)` is order isomorphic to `set.Iic a`; - `set.Iic (a : ℝ≥0∞)` is order isomorphic to `set.Iic a`; * Also, `ℝ≥0∞` is order isomorphic both to `Iic (1 : ℝ≥0∞)` and to the unit interval in `ℝ`. * Use the latter fact to golf `ennreal.second_countable_topology`. * Golf `ennreal.has_continuous_inv` using `order_iso.continuous`. * Improve definitional equalities for `equiv.subtype_subtype_equiv_subtype_exists`, `equiv.subtype_subtype_equiv_subtype_inter`, `equiv.subtype_subtype_equiv_subtype`, `equiv.set.sep`, use `simps`.