X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ ∞ ∈ (some '' s)ᶜ
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ IsOpen ((some '' s)ᶜ) ↔ IsClosed s ∧ IsCompact s
rw [isOpen_iff_of_mem, ← preimage_compl, compl_compl, preimage_image_eq _ coe_injective]
no goals
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ ∞ ∈ (some '' s)ᶜ
exact infty_not_mem_image_coe