English
In a locally compact regular space, given K compact and contained in open U, there exists an open V with K ⊆ V ⊆ closure(V) ⊆ U and closure(V) is compact.
Русский
В локально компактном регулярном пространстве, если компактное K вложено в открытое U, то существует открытое V such that K ⊆ V ⊆ closure(V) ⊆ U и closure(V) компактно.
LaTeX
$$$\text{In a locally compact regular space }X,\ \forall K,U\subset X,\ K\text{ compact},\ U\text{ open},\ K\subseteq U \Rightarrow \exists V,\ IsOpen(V) \land K\subseteq V \land \overline{V} \subseteq U \land \overline{V}\text{ compact}.$$$
Lean4
/-- In a locally compact regular space, given a compact set `K` inside an open set `U`, we can find
an open set `V` between these sets with compact closure: `K ⊆ V` and the closure of `V` is
inside `U`. -/
theorem exists_open_between_and_isCompact_closure [LocallyCompactSpace X] [RegularSpace X] {K U : Set X}
(hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V) :=
by
rcases exists_compact_closed_between hK hU hKU with ⟨L, L_compact, L_closed, KL, LU⟩
have A : closure (interior L) ⊆ L := by apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq)
refine ⟨interior L, isOpen_interior, KL, A.trans LU, ?_⟩
exact L_compact.closure_of_subset interior_subset
