X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ HasBasis (map some (coclosedCompact X) ⊔ pure ∞) (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ HasBasis (𝓝 ∞) (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
rw [nhds_infty_eq]
no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ HasBasis (map some (coclosedCompact X) ⊔ pure ∞) (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
exact (hasBasis_coclosedCompact.map _).sup_pure _