Compactness of the exterior of a set

In this file we prove that the exterior of a set (defined as the intersection of all of its neighborhoods) is a compact set if and only if the original set is a compact set.

theorem IsCompact.exterior_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsCompact (exterior s) ↔ IsCompact s

theorem IsCompact.exterior {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsCompact s → IsCompact (exterior s)

Alias of the reverse direction of IsCompact.exterior_iff.

theorem IsCompact.of_exterior {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsCompact (exterior s) → IsCompact s

Alias of the forward direction of IsCompact.exterior_iff.

@[deprecated IsCompact.exterior]

theorem Set.Finite.isCompact_exterior {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : s.Finite) : IsCompact (exterior s)