English
In a weakly locally compact space, every compact set is contained in the interior of some compact set.
Русский
В слабой локально компактной топологии каждый компактный набор содержится вInterior некоторого другого компактного набора.
LaTeX
$$$ \\exists K', \\ IsCompact(K') \\wedge K \\subseteq \\operatorname{interior}(K') $$$
Lean4
/-- In a weakly locally compact space,
every compact set is contained in the interior of a compact set. -/
theorem exists_compact_superset [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) :
∃ K', IsCompact K' ∧ K ⊆ interior K' :=
by
choose s hc hmem using fun x : X ↦ exists_compact_mem_nhds x
rcases hK.elim_nhds_subcover _ fun x _ ↦ interior_mem_nhds.2 (hmem x) with ⟨I, -, hIK⟩
refine ⟨⋃ x ∈ I, s x, I.isCompact_biUnion fun _ _ ↦ hc _, hIK.trans ?_⟩
exact iUnion₂_subset fun x hx ↦ interior_mono <| subset_iUnion₂ (s := fun x _ ↦ s x) x hx
