Commit 2022-06-24 01:29 ac2e9dbf

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.