no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ¬∞ ∈ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]