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.

theorem nhdsKer_singleton_eq_ker_nhds {X : Type u_2} [TopologicalSpace X] (x : X) : nhdsKer {x} = (nhds x).ker

@[simp]

theorem mem_nhdsKer_singleton {X : Type u_2} [TopologicalSpace X] {x y : X} : x ∈ nhdsKer {y} ↔ x ⤳ y

theorem nhdsKer_def {X : Type u_2} [TopologicalSpace X] (s : Set X) : nhdsKer s = ⋂₀ {t : Set X | IsOpen t ∧ s ⊆ t}

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

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

theorem subset_nhdsKer {X : Type u_2} [TopologicalSpace X] {s : Set X} : s ⊆ nhdsKer s

theorem nhdsKer_minimal {X : Type u_2} [TopologicalSpace X] {s t : Set X} (h₁ : s ⊆ t) (h₂ : IsOpen t) : nhdsKer s ⊆ t

theorem IsOpen.nhdsKer_eq {X : Type u_2} [TopologicalSpace X] {s : Set X} (h : IsOpen s) : nhdsKer s = s

theorem IsOpen.nhdsKer_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) : nhdsKer s ⊆ t ↔ s ⊆ t

@[simp]

theorem nhdsKer_iUnion {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] (s : ι → Set X) : nhdsKer (⋃ (i : ι), s i) = ⋃ (i : ι), nhdsKer (s i)

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)

@[simp]

theorem nhdsKer_union {X : Type u_2} [TopologicalSpace X] (s t : Set X) : nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t

@[simp]

theorem nhdsKer_sUnion {X : Type u_2} [TopologicalSpace X] (S : Set (Set X)) : nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s

theorem mem_nhdsKer_iff_specializes {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} : x ∈ nhdsKer s ↔ ∃ y ∈ s, x ⤳ y

theorem nhdsKer_mono {X : Type u_2} [TopologicalSpace X] : Monotone nhdsKer

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.

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

theorem nhdsKer_eq_nhdsKer_iff_nhdsSet {X : Type u_2} [TopologicalSpace X] {s t : Set X} : nhdsKer s = nhdsKer t ↔ nhdsSet s = nhdsSet t

theorem specializes_iff_nhdsKer_subset {X : Type u_2} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ nhdsKer {x} ⊆ nhdsKer {y}

theorem nhdsKer_iInter_subset {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] {s : ι → Set X} : nhdsKer (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), nhdsKer (s i)

theorem nhdsKer_inter_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} : nhdsKer (s ∩ t) ⊆ nhdsKer s ∩ nhdsKer t

theorem nhdsKer_sInter_subset {X : Type u_2} [TopologicalSpace X] {s : Set (Set X)} : nhdsKer (⋂₀ s) ⊆ ⋂ x ∈ s, nhdsKer x

@[simp]

theorem nhdsKer_empty {X : Type u_2} [TopologicalSpace X] : nhdsKer ∅ = ∅

@[simp]

theorem nhdsKer_univ {X : Type u_2} [TopologicalSpace X] : nhdsKer Set.univ = Set.univ

@[simp]

theorem nhdsKer_eq_empty {X : Type u_2} [TopologicalSpace X] {s : Set X} : nhdsKer s = ∅ ↔ s = ∅

@[simp]

theorem nhdsSet_nhdsKer {X : Type u_2} [TopologicalSpace X] (s : Set X) : nhdsSet (nhdsKer s) = nhdsSet s

@[simp]

theorem nhdsKer_nhdsKer {X : Type u_2} [TopologicalSpace X] (s : Set X) : nhdsKer (nhdsKer s) = nhdsKer s

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}

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

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}

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)