case intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.140885
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
x : α
K : Set α
hKc : IsCompact K
hxK : K ∈ 𝓝 x
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.140885
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
x : α
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
rcases exists_compact_mem_nhds x with ⟨K, hKc, hxK⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.140885
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
x : α
K : Set α
hKc : IsCompact K
hxK : K ∈ 𝓝 x
t : Set α
h1t : t ⊆ K
h2t : IsOpen t
h3t : x ∈ t
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
case intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.140885
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
x : α
K : Set α
hKc : IsCompact K
hxK : K ∈ 𝓝 x
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
rcases mem_nhds_iff.1 hxK with ⟨t, h1t, h2t, h3t⟩
no goals
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.140885
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
x : α
K : Set α
hKc : IsCompact K
hxK : K ∈ 𝓝 x
t : Set α
h1t : t ⊆ K
h2t : IsOpen t
h3t : x ∈ t
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
exact ⟨t, h2t, h3t, isCompact_closure_of_subset_compact hKc h1t⟩