isCompact_isClosed_basis_nhds — Mathlib

English

A weakly locally compact R1 space is locally compact.

Русский

Слабократно локально компактное R1-пространство является локально компактным.

LaTeX

$$LocallyCompactSpace X$$

Lean4

/-- In a (weakly) locally compact R₁ space, compact closed neighborhoods of a point `x`
form a basis of neighborhoods of `x`. -/
theorem isCompact_isClosed_basis_nhds (x : X) : (𝓝 x).HasBasis (fun K => K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·) :=
  let ⟨_L, hLc, hLx⟩ := exists_compact_mem_nhds x
  hLc.isCompact_isClosed_basis_nhds hLx

Похожие утверждения