Theorems · Theorem · general topology

IsCompact.separation_of_notMem

∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x : X} {t : Set X},
  IsCompact t → x ∉ t → ∃ U V, IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

In a T2Space X, for a compact set t and a point x outside t, there are open sets U, V that separate t and x.

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