refactor(order/{bounded, rel_classes}): Moved bounded into the set namespace (#11594)

As per the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/bounded.2Emono). Closes #11589.

Author: vihdzp

src/order/bounded.lean

@@ -15,6 +15,7 @@ the same ideas, or similar results with a few minor differences. The file is div
 different general ideas.
 -/
 
+namespace set
 variables {α : Type*} {r : α → α → Prop} {s t : set α}
 
 /-! ### Subsets of bounded and unbounded sets -/
@@ -328,3 +329,5 @@ theorem bounded_gt_inter_gt [linear_order α] [no_min_order α] (a : α) :
 theorem unbounded_gt_inter_gt [linear_order α] [no_min_order α] (a : α) :
   unbounded (>) (s ∩ {b | b < a}) ↔ unbounded (>) s :=
 @unbounded_lt_inter_lt (order_dual α) s _ _ a
+
+end set

src/order/rel_classes.lean

@@ -281,9 +281,11 @@ instance prod.lex.is_well_order [is_well_order α r] [is_well_order β s] :
   end,
   wf := prod.lex_wf is_well_order.wf is_well_order.wf }
 
-/-- An unbounded or cofinal set -/
+namespace set
+
+/-- An unbounded or cofinal set. -/
 def unbounded (r : α → α → Prop) (s : set α) : Prop := ∀ a, ∃ b ∈ s, ¬ r b a
-/-- A bounded or final set -/
+/-- A bounded or final set. Not to be confused with `metric.bounded`. -/
 def bounded (r : α → α → Prop) (s : set α) : Prop := ∃ a, ∀ b ∈ s, r b a
 
 @[simp] lemma not_bounded_iff {r : α → α → Prop} (s : set α) : ¬bounded r s ↔ unbounded r s :=
@@ -292,6 +294,8 @@ by simp only [bounded, unbounded, not_forall, not_exists, exists_prop, not_and,
 @[simp] lemma not_unbounded_iff {r : α → α → Prop} (s : set α) : ¬unbounded r s ↔ bounded r s :=
 by rw [not_iff_comm, not_bounded_iff]
 
+end set
+
 namespace prod
 
 instance is_refl_preimage_fst {r : α → α → Prop} [h : is_refl α r] :