English
In a locally compact space, for compact K ⊆ U with U open, there exists a compact L with K ⊆ interior L ⊆ L ⊆ U.
Русский
В локально компактном пространстве для компактного K ⊆ открытого U существует компактное L такое, что K ⊆ interior L ⊆ L ⊆ U.
LaTeX
$$$[LocallyCompactSpace\;X] {K: Set\;X} (hK:IsCompact K) (hU:IsOpen U) (h_KU: K\subseteq U)\Rightarrow \exists L, IsCompact L ∧ K\subseteq interior L ∧ L\subseteq U$$$
Lean4
/-- In a locally compact space, for every containment `K ⊆ U` of a compact set `K` in an open
set `U`, there is a compact neighborhood `L` such that `K ⊆ L ⊆ U`: equivalently, there is a
compact `L` such that `K ⊆ interior L` and `L ⊆ U`.
See also `exists_compact_closed_between`, in which one guarantees additionally that `L` is closed
if the space is regular. -/
theorem exists_compact_between [LocallyCompactSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) :
∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U :=
let ⟨L, hKL, hL, hLU⟩ := exists_mem_nhdsSet_isCompact_mapsTo continuous_id hK hU h_KU
⟨L, hL, subset_interior_iff_mem_nhdsSet.2 hKL, hLU⟩
