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

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.