Theorems · Theorem · general topology

exists_compact_subset

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

A reformulation of the definition of locally compact space: In a locally compact space, every open set containing x has a compact subset containing x in its interior.

Defined in

Mathlib.Topology.Compactness.LocallyCompact

Cited by

4 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceLocallyCompactSpace