Theorems · Theorem · general topology

IsCompact.disjoint_nhdsSet_nhds

∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x : X} {t : Set X},
  IsCompact t → x ∉ t → Disjoint (nhdsSet t) (nhds x)

In a T2Space X, for a compact set t and a point x outside t, 𝓝ˢ t and 𝓝 x are disjoint.

Defined in

Mathlib.Topology.Separation.Hausdorff

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2Space