English
In a locally compact space, every open set containing x contains a compact subset containing x in its interior.
Русский
В локально компактном пространстве каждая открытая окрестность точки содержит компактное подмножество, содержащее точку в своей внутренности.
LaTeX
$$$\forall X\,[TopologicalSpace\;X]\,[LocallyCompactSpace\;X]\ {x:X}\ {U:Set\;X}, IsOpen\;U\rightarrow x\in U\rightarrow\exists K\;IsCompact\;K\land x\in interior\;K\land K\subset U$$$
Lean4
/-- A reformulation of the definition of locally compact space: In a locally compact space,
every open set containing `x` has a compact subset containing `x` in its interior. -/
theorem exists_compact_subset [LocallyCompactSpace X] {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) :
∃ K : Set X, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U :=
by
rcases LocallyCompactSpace.local_compact_nhds x U (hU.mem_nhds hx) with ⟨K, h1K, h2K, h3K⟩
exact ⟨K, h3K, mem_interior_iff_mem_nhds.2 h1K, h2K⟩
