# Compactness of the neighborhoods kernel of a set #

In this file we prove that the neighborhoods kernel 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.

source
theorem IsCompact.nhdsKer_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} :
IsCompact (nhdsKer s) ↔ IsCompact s
source
@[deprecated IsCompact.nhdsKer_iff (since := "2025-07-09")]
theorem IsCompact.exterior_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} :
IsCompact (nhdsKer s) ↔ IsCompact s

Alias of `IsCompact.nhdsKer_iff`.

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

Alias of the reverse direction of `IsCompact.nhdsKer_iff`.

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

Alias of the forward direction of `IsCompact.nhdsKer_iff`.

source
@[deprecated IsCompact.of_nhdsKer (since := "2025-07-09")]
theorem IsCompact.of_exterior {X : Type u_1} [TopologicalSpace X] {s : Set X} :
IsCompact (nhdsKer s) → IsCompact s

Alias of the forward direction of `IsCompact.nhdsKer_iff`.

Alias of the forward direction of `IsCompact.nhdsKer_iff`.

source
@[deprecated IsCompact.nhdsKer (since := "2025-07-09")]
theorem IsCompact.exterior {X : Type u_1} [TopologicalSpace X] {s : Set X} :
IsCompact s → IsCompact (nhdsKer s)

Alias of the reverse direction of `IsCompact.nhdsKer_iff`.

Alias of the reverse direction of `IsCompact.nhdsKer_iff`.