# Commit 2022-06-24 01:29 ac2e9dbf

View on Github →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`

.