α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
h : RegularSpace α ↔ ∀ (a : α) (s : Set α), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
⊢ Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
have h := (regularSpace_TFAE α).out 0 2
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
h : RegularSpace α ↔ ∀ (a : α) (s : Set α), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
⊢ Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
exact h.mp ‹_› _ _