Theorem: uIoo_subset_uIcc (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ uIoo a b ⊆ uIcc a b
Tactic:
cases le_total a b <;> simp [uIoo, uIcc, Ioo_subset_Icc_self, *]
State after:
no goals