feat(Mathlib/Topology/Bases): subbasis closed under intersection is a basis (#12221)

We show that if a sub-basis is closed under finite intersections, then it is a basis for a topology.

As a corollary, if a sub-basis is closed under intersections, then inserting the universal set gives a basis for the topology.

An example application of this result is given in #12234



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Author: mans0954

Mathlib/Data/Set/Constructions.lean

@@ -82,4 +82,13 @@ theorem finiteInterClosure_insert {A : Set α} (cond : FiniteInter S) (P)
             constructor <;> simp (config := { contextual := true })⟩
 #align has_finite_inter.finite_inter_closure_insert FiniteInter.finiteInterClosure_insert
 
+open Set
+
+theorem mk₂ (h: ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ t ∈ S) :
+    FiniteInter (insert (univ : Set α) S) where
+  univ_mem := Set.mem_insert Set.univ S
+  inter_mem s hs t ht:= by
+    obtain ⟨(rfl | hs), (rfl | ht)⟩ := And.intro hs ht
+    all_goals aesop
+
 end FiniteInter

Mathlib/Topology/Bases.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
+import Mathlib.Data.Set.Constructions
 import Mathlib.Topology.Constructions
 import Mathlib.Topology.ContinuousOn
 
@@ -119,6 +120,18 @@ theorem isTopologicalBasis_of_subbasis {s : Set (Set α)} (hs : t = generateFrom
     exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩
 #align topological_space.is_topological_basis_of_subbasis TopologicalSpace.isTopologicalBasis_of_subbasis
 
+theorem isTopologicalBasis_of_subbasis_of_finiteInter {s : Set (Set α)} (hsg : t = generateFrom s)
+    (hsi : FiniteInter s) : IsTopologicalBasis s := by
+  convert isTopologicalBasis_of_subbasis hsg
+  refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_
+  rintro _ ⟨g, ⟨hg, hgs⟩, rfl⟩
+  lift g to Finset (Set α) using hg
+  exact hsi.finiteInter_mem g hgs
+
+theorem isTopologicalBasis_of_subbasis_of_inter {r : Set (Set α)} (hsg : t = generateFrom r)
+    (hsi : ∀ ⦃s⦄, s ∈ r → ∀ ⦃t⦄, t ∈ r → s ∩ t ∈ r) : IsTopologicalBasis (insert univ r) :=
+  isTopologicalBasis_of_subbasis_of_finiteInter (by simpa using hsg) (FiniteInter.mk₂ hsi)
+
 theorem IsTopologicalBasis.of_hasBasis_nhds {s : Set (Set α)}
     (h_nhds : ∀ a, (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id) : IsTopologicalBasis s where
   exists_subset_inter t₁ ht₁ t₂ ht₂ x hx := by

Mathlib/Topology/Order.lean

@@ -579,6 +579,18 @@ theorem le_induced_generateFrom {α β} [t : TopologicalSpace α] {b : Set (Set
   exact h
 #align le_induced_generate_from le_induced_generateFrom
 
+lemma generateFrom_insert_of_generateOpen {α : Type*} {s : Set (Set α)} {t : Set α}
+    (ht : GenerateOpen s t) : generateFrom (insert t s) = generateFrom s := by
+  refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)
+  rintro t (rfl | h)
+  · exact ht
+  · exact isOpen_generateFrom_of_mem h
+
+@[simp]
+lemma generateFrom_insert_univ {α : Type*} {s : Set (Set α)} :
+    generateFrom (insert univ s) = generateFrom s :=
+  generateFrom_insert_of_generateOpen .univ
+
 /-- This construction is left adjoint to the operation sending a topology on `α`
   to its neighborhood filter at a fixed point `a : α`. -/
 def nhdsAdjoint (a : α) (f : Filter α) : TopologicalSpace α where