English
For a fixed x in a (weakly) locally compact R1 space, there exists a neighborhood basis at x consisting of compact closed sets.
Русский
Для фиксированной точки x в слаб Locally компактном R1-пространстве существует база окрестностей в x из компактных замкнутых множеств.
LaTeX
$$(nhds x).HasBasis(K ↦ K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) (·)$$
Lean4
/-- If a point in an R₁ space has a compact neighborhood,
then it has a basis of compact closed neighborhoods. -/
theorem isCompact_isClosed_basis_nhds {x : X} {L : Set X} (hLc : IsCompact L) (hxL : L ∈ 𝓝 x) :
(𝓝 x).HasBasis (fun K ↦ K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·) :=
hasBasis_self.2 fun _U hU ↦
let ⟨K, hKx, hKc, hKU⟩ :=
exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds continuous_id (interior_mem_nhds.2 hU) hLc hxL
⟨closure K, mem_of_superset hKx subset_closure, ⟨hKc.closure, isClosed_closure⟩,
(hKc.closure_subset_of_isOpen isOpen_interior hKU).trans interior_subset⟩
