X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsOpen (range some)
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsClosed {∞}
rw [← compl_range_coe, isClosed_compl_iff]
no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsOpen (range some)
exact isOpen_range_coe