chore(data/real/ennreal, topology/instances/ennreal): change name of the order isomorphism for inv (#11959)

On [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/naming.20defs/near/271228611) it was decided that the name should be changed from `ennreal.inv_order_iso` to `order_iso.inv_ennreal` in order to better accord with the rest of the library.

Author: j-loreaux

src/data/real/ennreal.lean

@@ -1059,15 +1059,15 @@ inv_lt_iff_inv_lt.trans $ by rw [inv_one]
 
 /-- The inverse map `λ x, x⁻¹` is an order isomorphism between `ℝ≥0∞` and its `order_dual` -/
 @[simps apply]
-def inv_order_iso : ℝ≥0∞ ≃o order_dual ℝ≥0∞ :=
+def _root_.order_iso.inv_ennreal : ℝ≥0∞ ≃o order_dual ℝ≥0∞ :=
 { to_fun := λ x, x⁻¹,
   inv_fun := λ x, x⁻¹,
   left_inv := @ennreal.inv_inv,
   right_inv := @ennreal.inv_inv,
   map_rel_iff' := λ a b, ennreal.inv_le_inv }
 
 @[simp]
-lemma inv_order_iso_symm_apply : inv_order_iso.symm a = a⁻¹ := rfl
+lemma _root_.order_iso.inv_ennreal_symm_apply : order_iso.inv_ennreal.symm a = a⁻¹ := rfl
 
 lemma pow_le_pow_of_le_one {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
 begin

src/topology/instances/ennreal.lean

@@ -425,11 +425,11 @@ infi_mul_right' h (λ _, ‹nonempty ι›)
 
 lemma inv_map_infi {ι : Sort*} {x : ι → ℝ≥0∞} :
   (infi x)⁻¹ = (⨆ i, (x i)⁻¹) :=
-inv_order_iso.map_infi x
+order_iso.inv_ennreal.map_infi x
 
 lemma inv_map_supr {ι : Sort*} {x : ι → ℝ≥0∞} :
   (supr x)⁻¹ = (⨅ i, (x i)⁻¹) :=
-inv_order_iso.map_supr x
+order_iso.inv_ennreal.map_supr x
 
 lemma inv_limsup {ι : Sort*} {x : ι → ℝ≥0∞} {l : filter ι} :
   (l.limsup x)⁻¹ = l.liminf (λ i, (x i)⁻¹) :=