English
Let K be compact and U a neighborhood of K. There exists V open with K ⊆ V ⊆ closure(V) ⊆ U.
Русский
Пусть K компактно, U — окрестность K. Существeт открытое V с K ⊆ V ⊆ closure(V) ⊆ U.
LaTeX
$$$\forall K,U:\, IsCompact(K) \land U \in 𝓝(K) \Rightarrow \exists V:\, IsOpen(V) \land K \subset V \land closure(V) \subset U$$$
Lean4
theorem exists_isOpen_closure_subset {K U : Set X} (hK : IsCompact K) (hU : U ∈ 𝓝ˢ K) :
∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U :=
by
have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ) := by
simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet, ← subset_interior_iff_mem_nhdsSet] using hU
rcases ((hasBasis_nhdsSet _).disjoint_iff (hasBasis_nhdsSet _)).1 hd with ⟨V, ⟨hVo, hKV⟩, W, ⟨hW, hUW⟩, hVW⟩
refine ⟨V, hVo, hKV, Subset.trans ?_ (compl_subset_comm.1 hUW)⟩
exact closure_minimal hVW.subset_compl_right hW.isClosed_compl
