X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
this : ¬∞ ∈ sᶜ
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)
have : ∞ ∉ sᶜ := fun H => H h
no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
this : ¬∞ ∈ sᶜ
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)
rw [← isOpen_compl_iff, isOpen_iff_of_not_mem this, ← isOpen_compl_iff, preimage_compl]