no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsOpen s ↔ IsClosed ((some ⁻¹' s)ᶜ) ∧ IsCompact ((some ⁻¹' s)ᶜ)
simp only [isOpen_iff_of_mem' h, isClosed_compl_iff, and_comm]