chore(Topology/OrderClosed): review API (#10570)

- Generalize lemmas from `OrderClosedTopology`
  to `ClosedIciTopology` or `ClosedIicTopology`.
- Deprecate `isClosed_le'`/`isClosed_ge'`,
  use more readable `isClosed_Iic`/`isClosed_Ici` instead.

Mathlib/Topology/Instances/Real.lean

@@ -156,7 +156,7 @@ section
 theorem closure_of_rat_image_lt {q : ℚ} :
     closure (((↑) : ℚ → ℝ) '' { x | q < x }) = { r | ↑q ≤ r } :=
   Subset.antisymm
-    ((isClosed_ge' _).closure_subset_iff.2
+    (isClosed_Ici.closure_subset_iff.2
       (image_subset_iff.2 fun p h => le_of_lt <| (@Rat.cast_lt ℝ _ _ _).2 h))
     fun x hx => mem_closure_iff_nhds.2 fun t ht =>
       let ⟨ε, ε0, hε⟩ := Metric.mem_nhds_iff.1 ht

Mathlib/Topology/MetricSpace/Bounded.lean

@@ -98,7 +98,7 @@ theorem _root_.Bornology.IsBounded.subset_closedBall_lt (h : IsBounded s) (a : 
 
 theorem isBounded_closure_of_isBounded (h : IsBounded s) : IsBounded (closure s) :=
   let ⟨C, h⟩ := isBounded_iff.1 h
-  isBounded_iff.2 ⟨C, fun _a ha _b hb => (isClosed_le' C).closure_subset <|
+  isBounded_iff.2 ⟨C, fun _a ha _b hb => isClosed_Iic.closure_subset <|
     map_mem_closure₂ continuous_dist ha hb h⟩
 #align metric.bounded_closure_of_bounded Metric.isBounded_closure_of_isBounded