English
In a locally compact regular space, for every compact K contained in an open set U, there exists a compact closed set L with K ⊆ L ⊆ U (equivalently, K ⊆ interior L and L ⊆ U).
Русский
В локально компактном регулярном пространстве для любой компактной множества K, вложенного в открытое множество U, существует компактное замкнутое множество L такое, что K ⊆ L ⊆ U (эквивалентно K ⊆ interior(L) и L ⊆ U).
LaTeX
$$$\text{In a locally compact regular space }X,\ \text{for all compact }K\subseteq U\text{ with }U\text{ open and }K\subseteq U,\ \exists L\subset X\text{ such that }\operatorname{IsCompact}(L) \wedge \operatorname{IsClosed}(L) \wedge K \subset \operatorname{int}(L) \wedge L \subset U.$$$
Lean4
/-- In a (possibly non-Hausdorff) locally compact regular space, for every containment `K ⊆ U` of
a compact set `K` in an open set `U`, there is a compact closed neighborhood `L`
such that `K ⊆ L ⊆ U`: equivalently, there is a compact closed set `L` such
that `K ⊆ interior L` and `L ⊆ U`. -/
theorem exists_compact_closed_between [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K)
(hU : IsOpen U) (h_KU : K ⊆ U) : ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U :=
let ⟨L, L_comp, KL, LU⟩ := exists_compact_between hK hU h_KU
⟨closure L, L_comp.closure, isClosed_closure, KL.trans <| interior_mono subset_closure,
L_comp.closure_subset_of_isOpen hU LU⟩
