Theorems · Theorem · general topology

exists_compact_closed_between

∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X},
  IsCompact K → IsOpen U → K ⊆ U → ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U

In a (possibly non-Hausdorff) locally compact regular space, for every containment K ⊆ U of a compact set K in an open set U, there is a compact closed neighborhood L such that K ⊆ L ⊆ U: equivalently, there is a compact closed set L such that K ⊆ interior L and L ⊆ U.

Defined in

Mathlib.Topology.Separation.Regular

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyCompactSpaceRegularSpace