Documentation

Mathlib.Topology.NhdsKer

Neighborhoods kernel of a set #

In Mathlib/Topology/Defs/Filter.lean, nhdsKer s is defined to be the intersection of all neighborhoods of s. Note that this construction has no standard name in the literature.

In this file we prove basic properties of this operation.

source
theorem nhdsKer_singleton_eq_ker_nhds {X : Type u_2} [TopologicalSpace X] (x : X) :
nhdsKer {x} = (nhds x).ker
source
@[deprecated nhdsKer_singleton_eq_ker_nhds (since := "2025-07-09")]
theorem exterior_singleton_eq_ker_nhds {X : Type u_2} [TopologicalSpace X] (x : X) :
nhdsKer {x} = (nhds x).ker

Alias of nhdsKer_singleton_eq_ker_nhds.

source
@[simp]
theorem mem_nhdsKer_singleton {X : Type u_2} [TopologicalSpace X] {x y : X} :
x ∈ nhdsKer {y} ↔ x ⤳ y
source
@[deprecated mem_nhdsKer_singleton (since := "2025-07-09")]
theorem mem_exterior_singleton {X : Type u_2} [TopologicalSpace X] {x y : X} :
x ∈ nhdsKer {y} ↔ x ⤳ y

Alias of mem_nhdsKer_singleton.

source
theorem nhdsKer_def {X : Type u_2} [TopologicalSpace X] (s : Set X) :
nhdsKer s = ⋂₀ {t : Set X | IsOpen t ∧ s ⊆ t}
source
@[deprecated nhdsKer_def (since := "2025-07-09")]
theorem exterior_def {X : Type u_2} [TopologicalSpace X] (s : Set X) :
nhdsKer s = ⋂₀ {t : Set X | IsOpen t ∧ s ⊆ t}

Alias of nhdsKer_def.

source
theorem mem_nhdsKer {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} :
x ∈ nhdsKer s ↔ ∀ (U : Set X), IsOpen U → s ⊆ U → x ∈ U
source
@[deprecated mem_nhdsKer (since := "2025-07-09")]
theorem mem_exterior {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} :
x ∈ nhdsKer s ↔ ∀ (U : Set X), IsOpen U → s ⊆ U → x ∈ U

Alias of mem_nhdsKer.

source
theorem subset_nhdsKer_iff {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
s ⊆ nhdsKer t ↔ ∀ (U : Set X), IsOpen U → t ⊆ U → s ⊆ U
source
@[deprecated subset_nhdsKer_iff (since := "2025-07-09")]
theorem subset_exterior_iff {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
s ⊆ nhdsKer t ↔ ∀ (U : Set X), IsOpen U → t ⊆ U → s ⊆ U

Alias of subset_nhdsKer_iff.

source
theorem subset_nhdsKer {X : Type u_2} [TopologicalSpace X] {s : Set X} :
s ⊆ nhdsKer s
source
@[deprecated subset_nhdsKer (since := "2025-07-09")]
theorem subset_exterior {X : Type u_2} [TopologicalSpace X] {s : Set X} :
s ⊆ nhdsKer s

Alias of subset_nhdsKer.

source
theorem nhdsKer_minimal {X : Type u_2} [TopologicalSpace X] {s t : Set X} (h₁ : s ⊆ t) (h₂ : IsOpen t) :
nhdsKer s ⊆ t
source
@[deprecated nhdsKer_minimal (since := "2025-07-09")]
theorem exterior_minimal {X : Type u_2} [TopologicalSpace X] {s t : Set X} (h₁ : s ⊆ t) (h₂ : IsOpen t) :
nhdsKer s ⊆ t

Alias of nhdsKer_minimal.

source
theorem IsOpen.nhdsKer_eq {X : Type u_2} [TopologicalSpace X] {s : Set X} (h : IsOpen s) :
nhdsKer s = s
source
@[deprecated IsOpen.nhdsKer_eq (since := "2025-07-09")]
theorem IsOpen.exterior_eq {X : Type u_2} [TopologicalSpace X] {s : Set X} (h : IsOpen s) :
nhdsKer s = s

Alias of IsOpen.nhdsKer_eq.

source
theorem IsOpen.nhdsKer_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) :
nhdsKer s ⊆ t ↔ s ⊆ t
source
@[deprecated IsOpen.nhdsKer_subset (since := "2025-07-09")]
theorem IsOpen.exterior_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) :
nhdsKer s ⊆ t ↔ s ⊆ t

Alias of IsOpen.nhdsKer_subset.

source
@[simp]
theorem nhdsKer_iUnion {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] (s : ι → Set X) :
nhdsKer (⋃ (i : ι), s i) = ⋃ (i : ι), nhdsKer (s i)
source
@[deprecated nhdsKer_iUnion (since := "2025-07-09")]
theorem exterior_iUnion {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] (s : ι → Set X) :
nhdsKer (⋃ (i : ι), s i) = ⋃ (i : ι), nhdsKer (s i)

Alias of nhdsKer_iUnion.

source
theorem nhdsKer_biUnion {X : Type u_2} [TopologicalSpace X] {ι : Type u_3} (s : Set ι) (t : ι → Set X) :
nhdsKer (⋃ i ∈ s, t i) = ⋃ i ∈ s, nhdsKer (t i)
source
@[simp]
theorem nhdsKer_union {X : Type u_2} [TopologicalSpace X] (s t : Set X) :
nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t
source
@[deprecated nhdsKer_union (since := "2025-07-09")]
theorem exterior_union {X : Type u_2} [TopologicalSpace X] (s t : Set X) :
nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t

Alias of nhdsKer_union.

source
@[simp]
theorem nhdsKer_sUnion {X : Type u_2} [TopologicalSpace X] (S : Set (Set X)) :
nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s
source
@[deprecated nhdsKer_sUnion (since := "2025-07-09")]
theorem exterior_sUnion {X : Type u_2} [TopologicalSpace X] (S : Set (Set X)) :
nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s

Alias of nhdsKer_sUnion.

source
theorem mem_nhdsKer_iff_specializes {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} :
x ∈ nhdsKer s ↔ ∃ y ∈ s, x ⤳ y
source
@[deprecated mem_nhdsKer_iff_specializes (since := "2025-07-09")]
theorem mem_exterior_iff_specializes {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} :
x ∈ nhdsKer s ↔ ∃ y ∈ s, x ⤳ y

Alias of mem_nhdsKer_iff_specializes.

source
theorem nhdsKer_mono {X : Type u_2} [TopologicalSpace X] :
Monotone nhdsKer
source
@[deprecated nhdsKer_mono (since := "2025-07-09")]
theorem exterior_mono {X : Type u_2} [TopologicalSpace X] :
Monotone nhdsKer

Alias of nhdsKer_mono.

source
theorem nhdsKer_subset_nhdsKer {X : Type u_2} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) :
nhdsKer s ⊆ nhdsKer t

This name was used to be used for the Iff version, see nhdsKer_subset_nhdsKer_iff_nhdsSet.

source
@[deprecated nhdsKer_subset_nhdsKer (since := "2025-07-09")]
theorem exterior_subset_exterior {X : Type u_2} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) :
nhdsKer s ⊆ nhdsKer t

Alias of nhdsKer_subset_nhdsKer.

This name was used to be used for the Iff version, see nhdsKer_subset_nhdsKer_iff_nhdsSet.

source
@[simp]
theorem nhdsKer_subset_nhdsKer_iff_nhdsSet {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
nhdsKer s ⊆ nhdsKer t ↔ nhdsSet s ≤ nhdsSet t
source
@[deprecated nhdsKer_subset_nhdsKer_iff_nhdsSet (since := "2025-07-09")]
theorem exterior_subset_exterior_iff_nhdsSet {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
nhdsKer s ⊆ nhdsKer t ↔ nhdsSet s ≤ nhdsSet t

Alias of nhdsKer_subset_nhdsKer_iff_nhdsSet.

source
theorem nhdsKer_eq_nhdsKer_iff_nhdsSet {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
nhdsKer s = nhdsKer t ↔ nhdsSet s = nhdsSet t
source
@[deprecated nhdsKer_eq_nhdsKer_iff_nhdsSet (since := "2025-07-09")]
theorem exterior_eq_exterior_iff_nhdsSet {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
nhdsKer s = nhdsKer t ↔ nhdsSet s = nhdsSet t

Alias of nhdsKer_eq_nhdsKer_iff_nhdsSet.

source
theorem specializes_iff_nhdsKer_subset {X : Type u_2} [TopologicalSpace X] {x y : X} :
x ⤳ y ↔ nhdsKer {x} ⊆ nhdsKer {y}
source
@[deprecated specializes_iff_nhdsKer_subset (since := "2025-07-09")]
theorem specializes_iff_exterior_subset {X : Type u_2} [TopologicalSpace X] {x y : X} :
x ⤳ y ↔ nhdsKer {x} ⊆ nhdsKer {y}

Alias of specializes_iff_nhdsKer_subset.

source
theorem nhdsKer_iInter_subset {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] {s : ι → Set X} :
nhdsKer (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), nhdsKer (s i)
source
@[deprecated nhdsKer_iInter_subset (since := "2025-07-09")]
theorem exterior_iInter_subset {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] {s : ι → Set X} :
nhdsKer (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), nhdsKer (s i)

Alias of nhdsKer_iInter_subset.

source
theorem nhdsKer_inter_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
nhdsKer (s ∩ t) ⊆ nhdsKer s ∩ nhdsKer t
source
@[deprecated nhdsKer_inter_subset (since := "2025-07-09")]
theorem exterior_inter_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} :
nhdsKer (s ∩ t) ⊆ nhdsKer s ∩ nhdsKer t

Alias of nhdsKer_inter_subset.

source
theorem nhdsKer_sInter_subset {X : Type u_2} [TopologicalSpace X] {s : Set (Set X)} :
nhdsKer (⋂₀ s) ⊆ ⋂ x ∈ s, nhdsKer x
source
@[deprecated nhdsKer_sInter_subset (since := "2025-07-09")]
theorem exterior_sInter_subset {X : Type u_2} [TopologicalSpace X] {s : Set (Set X)} :
nhdsKer (⋂₀ s) ⊆ ⋂ x ∈ s, nhdsKer x

Alias of nhdsKer_sInter_subset.

source
@[simp]
theorem nhdsKer_empty {X : Type u_2} [TopologicalSpace X] :
nhdsKer ∅ = ∅
source
@[deprecated nhdsKer_empty (since := "2025-07-09")]
theorem exterior_empty {X : Type u_2} [TopologicalSpace X] :
nhdsKer ∅ = ∅

Alias of nhdsKer_empty.

source
@[simp]
theorem nhdsKer_univ {X : Type u_2} [TopologicalSpace X] :
nhdsKer Set.univ = Set.univ
source
@[deprecated nhdsKer_univ (since := "2025-07-09")]
theorem exterior_univ {X : Type u_2} [TopologicalSpace X] :
nhdsKer Set.univ = Set.univ

Alias of nhdsKer_univ.

source
@[simp]
theorem nhdsKer_eq_empty {X : Type u_2} [TopologicalSpace X] {s : Set X} :
nhdsKer s = ∅ ↔ s = ∅
source
@[deprecated nhdsKer_eq_empty (since := "2025-07-09")]
theorem exterior_eq_empty {X : Type u_2} [TopologicalSpace X] {s : Set X} :
nhdsKer s = ∅ ↔ s = ∅

Alias of nhdsKer_eq_empty.

source
@[simp]
theorem nhdsSet_nhdsKer {X : Type u_2} [TopologicalSpace X] (s : Set X) :
nhdsSet (nhdsKer s) = nhdsSet s
source
@[deprecated nhdsSet_nhdsKer (since := "2025-07-09")]
theorem nhdsSet_exterior {X : Type u_2} [TopologicalSpace X] (s : Set X) :
nhdsSet (nhdsKer s) = nhdsSet s

Alias of nhdsSet_nhdsKer.

source
@[simp]
theorem nhdsKer_nhdsKer {X : Type u_2} [TopologicalSpace X] (s : Set X) :
nhdsKer (nhdsKer s) = nhdsKer s
source
@[deprecated nhdsKer_nhdsKer (since := "2025-07-09")]
theorem exterior_exterior {X : Type u_2} [TopologicalSpace X] (s : Set X) :
nhdsKer (nhdsKer s) = nhdsKer s

Alias of nhdsKer_nhdsKer.

source
theorem nhdsKer_pair {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) :
nhdsKer {(x, y)} = nhdsKer {x} ×ˢ nhdsKer {y}
source
theorem nhdsKer_prod {X : Type u_2} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] (s : Set X) (t : Set Y) :
nhdsKer (s ×ˢ t) = nhdsKer s ×ˢ nhdsKer t
source
theorem nhdsKer_singleton_pi {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] (p : (i : ι) → X i) :
nhdsKer {p} = Set.univ.pi fun (i : ι) => nhdsKer {p i}
source
theorem nhdsKer_pi {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] (s : (i : ι) → Set (X i)) :
nhdsKer (Set.univ.pi s) = Set.univ.pi fun (i : ι) => nhdsKer (s i)