exact ⟨fun ⟨_, h, _, h'⟩ ↦ h h', fun h ↦ ⟨_, singleton_subset_iff.2 h, isOpen_singleton hx, rfl⟩⟩
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ (∃ t ⊆ s, IsOpen t ∧ x ∈ t) ↔ x ∈ s
no goals