exists_mem_nhds_isCompact_isClosed

English

Every point has a compact neighborhood that is closed and belongs to its neighborhood.

Русский

Каждая точка имеет компактную окрестность, которая замкнута и принадлежит к её окрестности.

LaTeX

$$∃ K ∈ nhds x, IsCompact K ∧ IsClosed K$$

Lean4

/-- In a (weakly) locally compact R₁ space, each point admits a compact closed neighborhood. -/
theorem exists_mem_nhds_isCompact_isClosed (x : X) : ∃ K ∈ 𝓝 x, IsCompact K ∧ IsClosed K :=
  (isCompact_isClosed_basis_nhds x).ex_mem

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