Theorems · Theorem · general topology

exists_compact_superset

∀ {X : Type u_1} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] {K : Set X},
  IsCompact K → ∃ K', IsCompact K' ∧ K ⊆ interior K'

In a weakly locally compact space, every compact set is contained in the interior of a compact set.

Defined in

Mathlib.Topology.Compactness.LocallyCompact

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceWeaklyLocallyCompactSpace