Theorem: uIoo_of_le (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c : ℝ
α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ uIoo a b = Ioo a b
Tactic:
rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
State after:
no goals