Theorems · Theorem · general topology

IsClosed.exists_closed_singleton

∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] [CompactSpace X] {S : Set X},
  IsClosed S → S.Nonempty → ∃ x ∈ S, IsClosed {x}

Given a closed set S in a compact T₀ space, there is some x ∈ S such that {x} is closed.

Defined in

Mathlib.Topology.Separation.Basic

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT0SpaceCompactSpace