chore(Order/UnorderedInterval): add basic uIoo lemmas (#31438)

Add a couple of lemmas about uIoo that are already present for uIcc. We also rename `uIoo_subset_uIcc` to `uIoo_subset_uIcc_self` for parity with the ordered version.

Author: b-mehta

Mathlib/Order/Interval/Set/UnorderedInterval.lean

@@ -352,6 +352,9 @@ lemma uIoo_of_gt (h : b < a) : uIoo a b = Ioo b a := uIoo_of_ge h.le
 
 lemma uIoo_self : uIoo a a = ∅ := by simp [uIoo]
 
+@[simp] lemma left_notMem_uIoo : a ∉ uIoo a b := by simp +contextual [uIoo, le_of_lt]
+@[simp] lemma right_notMem_uIoo : b ∉ uIoo a b := by simp +contextual [uIoo, le_of_lt]
+
 lemma Ioo_subset_uIoo : Ioo a b ⊆ uIoo a b := Ioo_subset_Ioo inf_le_left le_sup_right
 
 /-- Same as `Ioo_subset_uIoo` but with `Ioo a b` replaced by `Ioo b a`. -/
@@ -371,9 +374,23 @@ lemma uIoo_of_not_le (h : ¬a ≤ b) : uIoo a b = Ioo b a := uIoo_of_gt <| lt_of
 
 lemma uIoo_of_not_ge (h : ¬b ≤ a) : uIoo a b = Ioo a b := uIoo_of_lt <| lt_of_not_ge h
 
-theorem uIoo_subset_uIcc {α : Type*} [LinearOrder α] (a : α) (b : α) : uIoo a b ⊆ uIcc a b := by
+lemma uIoo_subset_uIcc_self : uIoo a b ⊆ uIcc a b := by
   simp [uIoo, uIcc, Ioo_subset_Icc_self]
 
+@[deprecated uIoo_subset_uIcc_self (since := "2025-11-09")]
+lemma uIoo_subset_uIcc (a b : α) : uIoo a b ⊆ uIcc a b := uIoo_subset_uIcc_self
+
+lemma uIoo_subset_Ioo (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) : uIoo a₁ b₁ ⊆ Ioo a₂ b₂ :=
+  Ioo_subset_Ioo (le_inf ha.1 hb.1) (sup_le ha.2 hb.2)
+
+@[simp] lemma nonempty_uIoo [DenselyOrdered α] : (uIoo a b).Nonempty ↔ a ≠ b := by
+  simp [uIoo, eq_comm]
+
+lemma uIoo_eq_union : uIoo a b = Ioo a b ∪ Ioo b a := by
+  rcases lt_or_ge a b with h | h
+  · simp [uIoo_of_lt, h, Ioo_eq_empty_of_le h.le]
+  · simp [uIoo_of_ge, h]
+
 end uIoo
 
 end LinearOrder