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.

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

@[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.

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.

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.

@[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.

@[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.