α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a✝ : α
s✝ : Set α
a : α
s : Set α
h : s ∈ 𝓝 a
h' : RegularSpace α ↔ ∀ (a : α) (s : Set α), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a✝ : α
s✝ : Set α
a : α
s : Set α
h : s ∈ 𝓝 a
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
have h' := (regularSpace_TFAE α).out 0 3
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a✝ : α
s✝ : Set α
a : α
s : Set α
h : s ∈ 𝓝 a
h' : RegularSpace α ↔ ∀ (a : α) (s : Set α), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
exact h'.mp ‹_› _ _ h