feat: Exterior of a set (#6982)

In an Alexandrov-discrete space, every set has a smallest neighborhood. We call this neighborhood the *exterior* of the set. It is completely analogous to the interior, except that all inclusions are reversed.

Mathlib/Order/Filter/Bases.lean

@@ -822,10 +822,9 @@ protected theorem HasBasis.biInter_mem {f : Set α → Set β} (h : HasBasis l p
   h.biInf_mem hf
 #align filter.has_basis.bInter_mem Filter.HasBasis.biInter_mem
 
-theorem HasBasis.sInter_sets (h : HasBasis l p s) : ⋂₀ l.sets = ⋂ (i) (_ : p i), s i := by
-  rw [sInter_eq_biInter]
-  exact h.biInter_mem monotone_id
-#align filter.has_basis.sInter_sets Filter.HasBasis.sInter_sets
+protected theorem HasBasis.ker (h : HasBasis l p s) : l.ker = ⋂ (i) (_ : p i), s i :=
+  l.ker_def.trans $ h.biInter_mem monotone_id
+#align filter.has_basis.sInter_sets Filter.HasBasis.ker
 
 variable {ι'' : Type*} [Preorder ι''] (l) (s'' : ι'' → Set α)
 

Mathlib/Order/Filter/Basic.lean

@@ -379,6 +379,10 @@ theorem mem_generate_iff {s : Set <| Set α} {U : Set α} :
     exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h
 #align filter.mem_generate_iff Filter.mem_generate_iff
 
+@[simp] lemma generate_singleton (s : Set α) : generate {s} = 𝓟 s :=
+le_antisymm (λ _t ht ↦ mem_of_superset (mem_generate_of_mem $ mem_singleton _) ht) $
+  le_generate_iff.2 $ singleton_subset_iff.2 Subset.rfl
+
 /-- `mk_of_closure s hs` constructs a filter on `α` whose elements set is exactly
 `s : Set (Set α)`, provided one gives the assumption `hs : (generate s).sets = s`. -/
 protected def mkOfClosure (s : Set (Set α)) (hs : (generate s).sets = s) : Filter α where
@@ -2893,10 +2897,12 @@ variable {ι : Sort*} {α β : Type*} {f g : Filter α} {s : Set α} {a : α}
 open Function Set
 
 /-- The *kernel* of a filter is the intersection of all its sets. -/
-def ker (f : Filter α) : Set α := ⋂ s ∈ f, s
+def ker (f : Filter α) : Set α := ⋂₀ f.sets
+
+lemma ker_def (f : Filter α) : f.ker = ⋂ s ∈ f, s := sInter_eq_biInter
 
-@[simp] lemma mem_ker : a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s := mem_iInter₂
-@[simp] lemma subset_ker : s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t := subset_iInter₂_iff
+@[simp] lemma mem_ker : a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s := mem_sInter
+@[simp] lemma subset_ker : s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t := subset_sInter_iff
 
 /-- `Filter.principal` forms a Galois coinsertion with `Filter.ker`. -/
 def gi_principal_ker : GaloisCoinsertion (𝓟 : Set α → Filter α) ker :=
@@ -2906,7 +2912,7 @@ GaloisConnection.toGaloisCoinsertion (λ s f ↦ by simp [principal_le_iff]) $ b
 lemma ker_mono : Monotone (ker : Filter α → Set α) := gi_principal_ker.gc.monotone_u
 lemma ker_surjective : Surjective (ker : Filter α → Set α) := gi_principal_ker.u_surjective
 
-@[simp] lemma ker_bot : ker (⊥ : Filter α) = ∅ := iInter₂_eq_empty_iff.2 λ _ ↦ ⟨∅, trivial, id⟩
+@[simp] lemma ker_bot : ker (⊥ : Filter α) = ∅ := sInter_eq_empty_iff.2 λ _ ↦ ⟨∅, trivial, id⟩
 @[simp] lemma ker_top : ker (⊤ : Filter α) = univ := gi_principal_ker.gc.u_top
 @[simp] lemma ker_eq_univ : ker f = univ ↔ f = ⊤ := gi_principal_ker.gc.u_eq_top.trans $ by simp
 @[simp] lemma ker_inf (f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g := gi_principal_ker.gc.u_inf

Mathlib/Order/Filter/Cofinite.lean

@@ -136,20 +136,17 @@ theorem disjoint_cofinite_right : Disjoint l cofinite ↔ ∃ s ∈ l, Set.Finit
   disjoint_comm.trans disjoint_cofinite_left
 #align filter.disjoint_cofinite_right Filter.disjoint_cofinite_right
 
-/-- If `l ≥ Filter.cofinite` is a countably generated filter, then `⋂₀ l.sets` is cocountable. -/
-theorem countable_compl_sInter_sets [l.IsCountablyGenerated] (h : cofinite ≤ l) :
-    Set.Countable (⋂₀ l.sets)ᶜ := by
+/-- If `l ≥ Filter.cofinite` is a countably generated filter, then `l.ker` is cocountable. -/
+theorem countable_compl_ker [l.IsCountablyGenerated] (h : cofinite ≤ l) : Set.Countable l.kerᶜ := by
   rcases exists_antitone_basis l with ⟨s, hs⟩
-  simp only [hs.sInter_sets, iInter_true, compl_iInter]
+  simp only [hs.ker, iInter_true, compl_iInter]
   exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _
 
 /-- If `f` tends to a countably generated filter `l` along `Filter.cofinite`,
-then for all but countably many elements, `f x ∈ ⋂₀ l.sets`. -/
-theorem Tendsto.countable_compl_preimage_sInter_sets {f : α → β}
+then for all but countably many elements, `f x ∈ l.ker`. -/
+theorem Tendsto.countable_compl_preimage_ker {f : α → β}
     {l : Filter β} [l.IsCountablyGenerated] (h : Tendsto f cofinite l) :
-    Set.Countable (f ⁻¹' (⋂₀ l.sets))ᶜ := by
-  erw [preimage_sInter, ← sInter_comap_sets]
-  exact countable_compl_sInter_sets h.le_comap
+    Set.Countable (f ⁻¹' l.ker)ᶜ := by rw [←ker_comap]; exact countable_compl_ker h.le_comap
 
 end Filter
 

Mathlib/Topology/AlexandrovDiscrete.lean

@@ -12,42 +12,253 @@ import Mathlib.Topology.SubsetProperties
 
 This file defines Alexandrov-discrete spaces, aka finitely generated spaces.
 
-A space is Alexandrov-discrete if the (arbitrary) intersection of open sets is open.
+A space is Alexandrov-discrete if the (arbitrary) intersection of open sets is open. As such,
+the intersection of all neighborhoods of a set is a neighborhood itself. Hence every set has a
+minimal neighborhood, which we call the *exterior* of the set.
+
+## Main declarations
+
+* `AlexandrovDiscrete`: Prop-valued typeclass for a topological space to be Alexandrov-discrete
+* `exterior`: Intersection of all neighborhoods of a set. When the space is Alexandrov-discrete,
+  this is the minimal neighborhood of the set.
+
+## Notes
+
+The "minimal neighborhood of a set" construction is not named in the literature. We chose the name
+"exterior" with analogy to the interior. `interior` and `exterior` have the same properties up to
+
 
 ## TODO
 
-Rest of the API
+Finite product of Alexandrov-discrete spaces is Alexandrov-discrete.
 
 ## Tags
 
 Alexandroff, discrete, finitely generated, fg space
 -/
 
-open Set TopologicalSpace
+open Filter Set TopologicalSpace
+open scoped Topology
 
 /-- A topological space is **Alexandrov-discrete** or **finitely generated** if the intersection of
 a family of open sets is open. -/
 class AlexandrovDiscrete (α : Type*) [TopologicalSpace α] : Prop where
   /-- The intersection of a family of open sets is an open set. Use `isOpen_sInter` in the root
   namespace instead. -/
-  protected isOpen_sInter : ∀ s : Set (Set α), (∀ t ∈ s, IsOpen t) → IsOpen (⋂₀ s)
+  protected isOpen_sInter : ∀ S : Set (Set α), (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
+
+variable {ι : Sort*} {κ : ι → Sort*} {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
+
+instance DiscreteTopology.toAlexandrovDiscrete [DiscreteTopology α] : AlexandrovDiscrete α where
+  isOpen_sInter _ _ := isOpen_discrete _
+
+instance Finite.toAlexandrovDiscrete [Finite α] : AlexandrovDiscrete α where
+  isOpen_sInter S := (toFinite S).isOpen_sInter
 
-variable {ι : Sort*} {α : Type*} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)}
-  {f : ι → Set α}
+section AlexandrovDiscrete
+variable [AlexandrovDiscrete α] {S : Set (Set α)} {f : ι → Set α}
 
 lemma isOpen_sInter : (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S) := AlexandrovDiscrete.isOpen_sInter _
 
 lemma isOpen_iInter (hf : ∀ i, IsOpen (f i)) : IsOpen (⋂ i, f i) :=
 isOpen_sInter $ forall_range_iff.2 hf
 
+lemma isOpen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsOpen (f i j)) :
+  IsOpen (⋂ i, ⋂ j, f i j) :=
+isOpen_iInter λ _ ↦ isOpen_iInter $ hf _
+
 lemma isClosed_sUnion (hS : ∀ s ∈ S, IsClosed s) : IsClosed (⋃₀ S) := by
   simp only [←isOpen_compl_iff, compl_sUnion] at hS ⊢; exact isOpen_sInter $ ball_image_iff.2 hS
 
 lemma isClosed_iUnion (hf : ∀ i, IsClosed (f i)) : IsClosed (⋃ i, f i) :=
 isClosed_sUnion $ forall_range_iff.2 hf
 
+lemma isClosed_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClosed (f i j)) :
+  IsClosed (⋃ i, ⋃ j, f i j) :=
+isClosed_iUnion λ _ ↦ isClosed_iUnion $ hf _
+
+lemma isClopen_sInter (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋂₀ S) :=
+⟨isOpen_sInter λ s hs ↦ (hS s hs).1, isClosed_sInter λ s hs ↦ (hS s hs).2⟩
+
+lemma isClopen_iInter (hf : ∀ i, IsClopen (f i)) : IsClopen (⋂ i, f i) :=
+⟨isOpen_iInter λ i ↦ (hf i).1, isClosed_iInter λ i ↦ (hf i).2⟩
+
+lemma isClopen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) :
+  IsClopen (⋂ i, ⋂ j, f i j) :=
+isClopen_iInter λ _ ↦ isClopen_iInter $ hf _
+
 lemma isClopen_sUnion (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋃₀ S) :=
 ⟨isOpen_sUnion λ s hs ↦ (hS s hs).1, isClosed_sUnion λ s hs ↦ (hS s hs).2⟩
 
 lemma isClopen_iUnion (hf : ∀ i, IsClopen (f i)) : IsClopen (⋃ i, f i) :=
 ⟨isOpen_iUnion λ i ↦ (hf i).1, isClosed_iUnion λ i ↦ (hf i).2⟩
+
+lemma isClopen_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) :
+  IsClopen (⋃ i, ⋃ j, f i j) :=
+isClopen_iUnion λ _ ↦ isClopen_iUnion $ hf _
+
+lemma interior_iInter (f : ι → Set α) : interior (⋂ i, f i) = ⋂ i, interior (f i) :=
+(interior_maximal (iInter_mono λ _ ↦ interior_subset) $ isOpen_iInter λ _ ↦
+  isOpen_interior).antisymm' $ subset_iInter λ _ ↦ interior_mono $ iInter_subset _ _
+
+lemma interior_sInter (S : Set (Set α)) : interior (⋂₀ S) = ⋂ s ∈ S, interior s := by
+  simp_rw [sInter_eq_biInter, interior_iInter]
+
+lemma closure_iUnion (f : ι → Set α) : closure (⋃ i, f i) = ⋃ i, closure (f i) :=
+  compl_injective $ by simpa only [←interior_compl, compl_iUnion] using interior_iInter λ i ↦ (f i)ᶜ
+
+lemma closure_sUnion (S : Set (Set α)) : closure (⋃₀ S) = ⋃ s ∈ S, closure s := by
+  simp_rw [sUnion_eq_biUnion, closure_iUnion]
+
+end AlexandrovDiscrete
+
+variable {s t : Set α} {a x y : α}
+
+/-- The *exterior* of a set is the intersection of all its neighborhoods. In an Alexandrov-discrete
+space, this is the smallest neighborhood of the set.
+
+Note that this construction is unnamed in the literature. We choose the name in analogy to
+`interior`. -/
+def exterior (s : Set α) : Set α := (𝓝ˢ s).ker
+
+lemma exterior_singleton_eq_ker_nhds (a : α) : exterior {a} = (𝓝 a).ker := by simp [exterior]
+
+lemma exterior_def (s : Set α) : exterior s = ⋂₀ {t : Set α | IsOpen t ∧ s ⊆ t} :=
+  (hasBasis_nhdsSet _).ker.trans sInter_eq_biInter.symm
+
+lemma mem_exterior : a ∈ exterior s ↔ ∀ U, IsOpen U → s ⊆ U → a ∈ U := by simp [exterior_def]
+
+lemma subset_exterior_iff : s ⊆ exterior t ↔ ∀ U, IsOpen U → t ⊆ U → s ⊆ U := by
+  simp [exterior_def]
+
+lemma subset_exterior : s ⊆ exterior s := subset_exterior_iff.2 $ λ _ _ ↦ id
+
+lemma exterior_minimal (h₁ : s ⊆ t) (h₂ : IsOpen t) : exterior s ⊆ t := by
+  rw [exterior_def]; exact sInter_subset_of_mem ⟨h₂, h₁⟩
+
+lemma IsOpen.exterior_eq (h : IsOpen s) : exterior s = s :=
+(exterior_minimal Subset.rfl h).antisymm subset_exterior
+
+lemma IsOpen.exterior_subset_iff (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t :=
+⟨subset_exterior.trans, λ h ↦ exterior_minimal h ht⟩
+
+@[mono] lemma exterior_mono : Monotone (exterior : Set α → Set α) :=
+λ _s _t h ↦ ker_mono $ nhdsSet_mono h
+
+@[simp] lemma exterior_empty : exterior (∅ : Set α) = ∅ := isOpen_empty.exterior_eq
+@[simp] lemma exterior_univ : exterior (univ : Set α) = univ := isOpen_univ.exterior_eq
+
+@[simp] lemma exterior_eq_empty : exterior s = ∅ ↔ s = ∅ :=
+⟨eq_bot_mono subset_exterior, by rintro rfl; exact exterior_empty⟩
+
+variable [AlexandrovDiscrete α] [AlexandrovDiscrete β]
+
+@[simp] lemma isOpen_exterior : IsOpen (exterior s) := by
+  rw [exterior_def]; exact isOpen_sInter $ λ _ ↦ And.left
+
+lemma exterior_mem_nhdsSet : exterior s ∈ 𝓝ˢ s := isOpen_exterior.mem_nhdsSet.2 subset_exterior
+
+@[simp] lemma exterior_eq_iff_isOpen : exterior s = s ↔ IsOpen s :=
+  ⟨λ h ↦ h ▸ isOpen_exterior, IsOpen.exterior_eq⟩
+
+@[simp] lemma exterior_subset_iff_isOpen : exterior s ⊆ s ↔ IsOpen s := by
+  simp only [exterior_eq_iff_isOpen.symm, Subset.antisymm_iff, subset_exterior, and_true]
+
+lemma exterior_subset_iff : exterior s ⊆ t ↔ ∃ U, IsOpen U ∧ s ⊆ U ∧ U ⊆ t :=
+  ⟨λ h ↦ ⟨exterior s, isOpen_exterior, subset_exterior, h⟩,
+    λ ⟨_U, hU, hsU, hUt⟩ ↦ (exterior_minimal hsU hU).trans hUt⟩
+
+lemma exterior_subset_iff_mem_nhdsSet : exterior s ⊆ t ↔ t ∈ 𝓝ˢ s :=
+exterior_subset_iff.trans mem_nhdsSet_iff_exists.symm
+
+lemma exterior_singleton_subset_iff_mem_nhds : exterior {a} ⊆ t ↔ t ∈ 𝓝 a := by
+  simp [exterior_subset_iff_mem_nhdsSet]
+
+lemma IsOpen.exterior_subset (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t :=
+  ⟨subset_exterior.trans, λ h ↦ exterior_minimal h ht⟩
+
+lemma gc_exterior_interior : GaloisConnection (exterior : Set α → Set α) interior :=
+  λ s t ↦ by simp [exterior_subset_iff, subset_interior_iff]
+
+@[simp] lemma exterior_exterior (s : Set α) : exterior (exterior s) = exterior s :=
+  isOpen_exterior.exterior_eq
+
+@[simp] lemma exterior_union (s t : Set α) : exterior (s ∪ t) = exterior s ∪ exterior t :=
+  gc_exterior_interior.l_sup
+
+@[simp] lemma nhdsSet_exterior (s : Set α) : 𝓝ˢ (exterior s) = 𝓝ˢ s := by
+  ext t; simp_rw [←exterior_subset_iff_mem_nhdsSet, exterior_exterior]
+
+@[simp] lemma principal_exterior (s : Set α) : 𝓟 (exterior s) = 𝓝ˢ s := by
+  rw [←nhdsSet_exterior, isOpen_exterior.nhdsSet_eq]
+
+@[simp] lemma exterior_subset_exterior : exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t := by
+  refine ⟨?_, λ h ↦ ker_mono h⟩
+  simp_rw [le_def, ←exterior_subset_iff_mem_nhdsSet]
+  exact λ h u ↦ h.trans
+
+lemma specializes_iff_exterior_subset : x ⤳ y ↔ exterior {x} ⊆ exterior {y} := by
+  simp [Specializes]
+
+lemma isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s → x ∈ s := by
+  refine' ⟨λ hs x y hxy ↦ hxy.mem_open hs, λ hs ↦ _⟩
+  simp_rw [specializes_iff_exterior_subset] at hs
+  simp_rw [isOpen_iff_mem_nhds, mem_nhds_iff]
+  rintro a ha
+  refine ⟨_, λ b hb ↦ hs _ _ ?_ ha, isOpen_exterior, subset_exterior $ mem_singleton _⟩
+  rwa [isOpen_exterior.exterior_subset, singleton_subset_iff]
+
+lemma Set.Finite.isCompact_exterior (hs : s.Finite) : IsCompact (exterior s) := by
+  classical
+  refine isCompact_of_finite_subcover λ f hf hsf ↦ ?_
+  choose g hg using λ a (ha : a ∈ exterior s) ↦ mem_iUnion.1 (hsf ha)
+  refine ⟨hs.toFinset.attach.image λ a ↦ g a.1 $ subset_exterior $ (Finite.mem_toFinset _).1 a.2,
+    (isOpen_iUnion λ i ↦ isOpen_iUnion ?_).exterior_subset.2 ?_⟩
+  exact λ _ ↦ hf _
+  refine λ a ha ↦ mem_iUnion₂.2 ⟨_, ?_, hg _ $ subset_exterior ha⟩
+  simp only [Finset.mem_image, Finset.mem_attach, true_and, Subtype.exists, Finite.mem_toFinset]
+  exact ⟨a, ha, rfl⟩
+
+lemma Inducing.alexandrovDiscrete {f : β → α} (h : Inducing f) : AlexandrovDiscrete β where
+  isOpen_sInter S hS := by
+    simp_rw [h.isOpen_iff] at hS ⊢
+    choose U hU htU using hS
+    refine ⟨_, isOpen_iInter₂ hU, ?_⟩
+    simp_rw [preimage_iInter, htU, sInter_eq_biInter]
+
+lemma alexandrovDiscrete_coinduced {β : Type*} {f : α → β} :
+  @AlexandrovDiscrete β (coinduced f ‹_›) :=
+@AlexandrovDiscrete.mk β (coinduced f ‹_›) λ S hS ↦ by
+  rw [isOpen_coinduced, preimage_sInter]; exact isOpen_iInter₂ hS
+
+lemma AlexandrovDiscrete.sup {t₁ t₂ : TopologicalSpace α} (_ : @AlexandrovDiscrete α t₁)
+  (_ : @AlexandrovDiscrete α t₂) :
+  @AlexandrovDiscrete α (t₁ ⊔ t₂) :=
+@AlexandrovDiscrete.mk α (t₁ ⊔ t₂) λ _S hS ↦
+  ⟨@isOpen_sInter _ t₁ _ _ λ _s hs ↦ (hS _ hs).1, isOpen_sInter λ _s hs ↦ (hS _ hs).2⟩
+
+lemma alexandrovDiscrete_iSup {t : ι → TopologicalSpace α} (_ : ∀ i, @AlexandrovDiscrete α (t i)) :
+  @AlexandrovDiscrete α (⨆ i, t i) :=
+@AlexandrovDiscrete.mk α (⨆ i, t i) λ _S hS ↦ isOpen_iSup_iff.2 λ i ↦ @isOpen_sInter _ (t i) _ _
+  λ _s hs ↦ isOpen_iSup_iff.1 (hS _ hs) _
+
+instance AlexandrovDiscrete.toFirstCountable : FirstCountableTopology α where
+  nhds_generated_countable a := ⟨{exterior {a}}, countable_singleton _, by simp⟩
+
+instance AlexandrovDiscrete.toLocallyCompactSpace : LocallyCompactSpace α where
+  local_compact_nhds a _U hU := ⟨exterior {a},
+    isOpen_exterior.mem_nhds $ subset_exterior $ mem_singleton _,
+      exterior_singleton_subset_iff_mem_nhds.2 hU, (finite_singleton _).isCompact_exterior⟩
+
+instance Subtype.instAlexandrovDiscrete {p : α → Prop} : AlexandrovDiscrete {a // p a} :=
+inducing_subtype_val.alexandrovDiscrete
+
+instance Quotient.instAlexandrovDiscrete {s : Setoid α} : AlexandrovDiscrete (Quotient s) :=
+alexandrovDiscrete_coinduced
+
+instance Sum.instAlexandrovDiscrete : AlexandrovDiscrete (α ⊕ β) :=
+alexandrovDiscrete_coinduced.sup alexandrovDiscrete_coinduced
+
+instance Sigma.instAlexandrovDiscrete {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
+  [∀ i, AlexandrovDiscrete (π i)] : AlexandrovDiscrete (Σ i, π i) :=
+alexandrovDiscrete_iSup λ _ ↦ alexandrovDiscrete_coinduced

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

@@ -1266,7 +1266,7 @@ theorem Summable.tendsto_atTop_zero {f : ℕ → G} (hf : Summable f) : Tendsto
 
 theorem Summable.countable_support [TopologicalSpace.FirstCountableTopology G] [T1Space G]
     (hf : Summable f) : f.support.Countable := by
-  simpa only [sInter_sets_nhds] using hf.tendsto_cofinite_zero.countable_compl_preimage_sInter_sets
+  simpa only [ker_nhds] using hf.tendsto_cofinite_zero.countable_compl_preimage_ker
 
 end TopologicalGroup
 

Mathlib/Topology/Bases.lean

@@ -63,7 +63,7 @@ namespace TopologicalSpace
 
 universe u
 
-variable {α : Type u} [t : TopologicalSpace α]
+variable {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s : Set α}
 
 /-- A topological basis is one that satisfies the necessary conditions so that
   it suffices to take unions of the basis sets to get a topology (without taking
@@ -208,6 +208,15 @@ theorem IsTopologicalBasis.open_eq_iUnion {B : Set (Set α)} (hB : IsTopological
     apply hB.open_eq_sUnion' ou, fun s => And.left s.2⟩
 #align topological_space.is_topological_basis.open_eq_Union TopologicalSpace.IsTopologicalBasis.open_eq_iUnion
 
+lemma IsTopologicalBasis.subset_of_forall_subset {t : Set α} (hB : IsTopologicalBasis B)
+  (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t) : s ⊆ t := by
+  rw [hB.open_eq_sUnion' hs]; simpa [sUnion_subset_iff]
+
+lemma IsTopologicalBasis.eq_of_forall_subset_iff {t : Set α} (hB : IsTopologicalBasis B)
+  (hs : IsOpen s) (ht : IsOpen t) (h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t) : s = t := by
+  rw [hB.open_eq_sUnion' hs, hB.open_eq_sUnion' ht]
+  exact congr_arg _ (Set.ext λ U ↦ and_congr_right $ h _)
+
 /-- A point `a` is in the closure of `s` iff all basis sets containing `a` intersect `s`. -/
 theorem IsTopologicalBasis.mem_closure_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α}
     {a : α} : a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty :=

Mathlib/Topology/Basic.lean

@@ -327,6 +327,9 @@ theorem subset_interior_iff {s t : Set α} : t ⊆ interior s ↔ ∃ U, IsOpen
     htU.trans (interior_maximal hUs hU)⟩
 #align subset_interior_iff subset_interior_iff
 
+lemma interior_subset_iff : interior s ⊆ t ↔ ∀ U, IsOpen U → U ⊆ s → U ⊆ t := by
+  simp [interior]
+
 @[mono]
 theorem interior_mono {s t : Set α} (h : s ⊆ t) : interior s ⊆ interior t :=
   interior_maximal (Subset.trans interior_subset h) isOpen_interior

Mathlib/Topology/Inseparable.lean

@@ -109,8 +109,8 @@ alias ⟨Specializes.nhds_le_nhds, _⟩ := specializes_iff_nhds
 alias ⟨Specializes.pure_le_nhds, _⟩ := specializes_iff_pure
 #align specializes.pure_le_nhds Specializes.pure_le_nhds
 
-theorem sInter_nhds_sets_eq_specializes : ⋂₀ (𝓝 x).sets = {y | y ⤳ x} :=
-  Set.ext fun _ ↦ specializes_iff_pure.symm
+theorem ker_nhds_eq_specializes : (𝓝 x).ker = {y | y ⤳ x} := by
+  ext; simp [specializes_iff_pure, le_def]
 
 theorem specializes_iff_forall_open : x ⤳ y ↔ ∀ s : Set X, IsOpen s → y ∈ s → x ∈ s :=
   (specializes_TFAE x y).out 0 2