Theorem: mem_uIoo (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ t ∈ uIoo a b ↔ a < t ∧ t < b ∨ b < t ∧ t < a
Tactic:
simp [uIoo_eq_union]
State after:
no goals