feat(topology): missing lemmas for Kyle (#11076)

Discussion [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Continuous.20bijective.20from.20compact.20to.20T1.20implies.20homeomorphis) revealed gaps in library. This PR fills those gaps and related ones discovered on the way. It will simplify #11072. Note that it unprotects `topological_space.nhds_adjoint` and puts it into the root namespace. I guess this was protected because it was seen only as a technical tools to prove properties of `nhds`.

src/data/set/finite.lean

@@ -325,6 +325,10 @@ h.inter_of_left t
 theorem finite.inf_of_right {s : set α} (h : finite s) (t : set α) : finite (t ⊓ s) :=
 h.inter_of_right t
 
+lemma finite.sInter {α : Type*} {s : set (set α)} {t : set α} (ht : t ∈ s)
+  (hf : t.finite) : (⋂₀s).finite :=
+hf.subset (sInter_subset_of_mem ht)
+
 protected theorem infinite.mono {s t : set α} (h : s ⊆ t) : infinite s → infinite t :=
 mt (λ ht, ht.subset h)
 

src/order/filter/ultrafilter.lean

@@ -151,6 +151,18 @@ instance : has_pure ultrafilter :=
 instance [inhabited α] : inhabited (ultrafilter α) := ⟨pure (default _)⟩
 instance [nonempty α] : nonempty (ultrafilter α) := nonempty.map pure infer_instance
 
+lemma eq_principal_of_finite_mem {f : ultrafilter α} {s : set α} (h : s.finite) (h' : s ∈ f) :
+  ∃ x ∈ s, (f : filter α) = pure x :=
+begin
+  rw ← bUnion_of_singleton s at h',
+  rcases (ultrafilter.finite_bUnion_mem_iff h).mp h' with ⟨a, has, haf⟩,
+  use [a, has],
+  change (f : filter α) = (pure a : ultrafilter α),
+  rw [ultrafilter.coe_inj, ← ultrafilter.coe_le_coe],
+  change (f : filter α) ≤ pure a,
+  rwa [← principal_singleton, le_principal_iff]
+end
+
 /-- Monadic bind for ultrafilters, coming from the one on filters
 defined in terms of map and join.-/
 def bind (f : ultrafilter α) (m : α → ultrafilter β) : ultrafilter β :=

src/topology/basic.lean

@@ -909,6 +909,18 @@ theorem is_open_iff_ultrafilter {s : set α} :
   is_open s ↔ (∀ (x ∈ s) (l : ultrafilter α), ↑l ≤ 𝓝 x → s ∈ l) :=
 by simp_rw [is_open_iff_mem_nhds, ← mem_iff_ultrafilter]
 
+lemma is_open_singleton_iff_nhds_eq_pure {α : Type*} [topological_space α] (a : α) :
+  is_open ({a} : set α) ↔ 𝓝 a = pure a :=
+begin
+  split,
+  { intros h,
+    apply le_antisymm _ (pure_le_nhds a),
+    rw le_pure_iff,
+    exact h.mem_nhds (mem_singleton a) },
+  { intros h,
+    simp [is_open_iff_nhds, h] }
+end
+
 lemma mem_closure_iff_frequently {s : set α} {a : α} : a ∈ closure s ↔ ∃ᶠ x in 𝓝 a, x ∈ s :=
 by rw [filter.frequently, filter.eventually, ← mem_interior_iff_mem_nhds,
   closure_eq_compl_interior_compl]; refl

src/topology/constructions.lean

@@ -110,6 +110,40 @@ theorem nhds_subtype (s : set α) (a : {x // x ∈ s}) :
 nhds_induced coe a
 
 end topα
+/-- The topology whose open sets are the empty set and the sets with finite complements. -/
+def cofinite_topology (α : Type*) : topological_space α :=
+{ is_open := λ s, s.nonempty → set.finite sᶜ,
+  is_open_univ := by simp,
+  is_open_inter := λ s t, begin
+    classical,
+    rintros hs ht ⟨x, hxs, hxt⟩,
+    haveI := set.finite.fintype (hs ⟨x, hxs⟩),
+    haveI := set.finite.fintype (ht ⟨x, hxt⟩),
+    rw compl_inter,
+    exact set.finite.intro (sᶜ.fintype_union tᶜ),
+  end,
+  is_open_sUnion := begin
+    rintros s h ⟨x, t, hts, hzt⟩,
+    rw set.compl_sUnion,
+    apply set.finite.sInter _ (h t hts ⟨x, hzt⟩),
+    simp [hts]
+    end }
+
+lemma nhds_cofinite {α : Type*} (a : α) :
+  @nhds α (cofinite_topology α) a = pure a ⊔ cofinite :=
+begin
+  ext U,
+  rw mem_nhds_iff,
+  split,
+  { rintro ⟨V, hVU, V_op, haV⟩,
+    exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩ },
+  { rintros ⟨hU : a ∈ U, hU' : (Uᶜ).finite⟩,
+    exact ⟨U, subset.rfl, λ h, hU', hU⟩ }
+end
+
+lemma mem_nhds_cofinite {α : Type*} {a : α} {s : set α} :
+  s ∈ @nhds α (cofinite_topology α) a ↔ a ∈ s ∧ sᶜ.finite :=
+by simp [nhds_cofinite]
 
 end constructions
 

src/topology/order.lean

@@ -479,20 +479,83 @@ end
 
 /-- This construction is left adjoint to the operation sending a topology on `α`
   to its neighborhood filter at a fixed point `a : α`. -/
-protected def topological_space.nhds_adjoint (a : α) (f : filter α) : topological_space α :=
+def nhds_adjoint (a : α) (f : filter α) : topological_space α :=
 { is_open        := λs, a ∈ s → s ∈ f,
   is_open_univ   := assume s, univ_mem,
   is_open_inter  := assume s t hs ht ⟨has, hat⟩, inter_mem (hs has) (ht hat),
   is_open_sUnion := assume k hk ⟨u, hu, hau⟩, mem_of_superset (hk u hu hau)
     (subset_sUnion_of_mem hu) }
 
 lemma gc_nhds (a : α) :
-  galois_connection  (topological_space.nhds_adjoint a) (λt, @nhds α t a) :=
+  galois_connection (nhds_adjoint a) (λt, @nhds α t a) :=
 assume f t, by { rw le_nhds_iff, exact ⟨λ H s hs has, H _ has hs, λ H s has hs, H _ hs has⟩ }
 
 lemma nhds_mono {t₁ t₂ : topological_space α} {a : α} (h : t₁ ≤ t₂) :
   @nhds α t₁ a ≤ @nhds α t₂ a := (gc_nhds a).monotone_u h
 
+lemma le_iff_nhds {α : Type*} (t t' : topological_space α) :
+  t ≤ t' ↔ ∀ x, @nhds α t x ≤ @nhds α t' x :=
+⟨λ h x, nhds_mono h, le_of_nhds_le_nhds⟩
+
+lemma nhds_adjoint_nhds {α : Type*} (a : α) (f : filter α) :
+  @nhds α (nhds_adjoint a f) a = pure a ⊔ f :=
+begin
+  ext U,
+  rw mem_nhds_iff,
+  split,
+  { rintros ⟨t, htU, ht, hat⟩,
+    exact ⟨htU hat, mem_of_superset (ht hat) htU⟩},
+  { rintros ⟨haU, hU⟩,
+    exact ⟨U, subset.rfl, λ h, hU, haU⟩ }
+end
+
+lemma nhds_adjoint_nhds_of_ne {α : Type*} (a : α) (f : filter α) {b : α} (h : b ≠ a) :
+  @nhds α (nhds_adjoint a f) b = pure b :=
+begin
+  apply le_antisymm,
+  { intros U hU,
+    rw mem_nhds_iff,
+    use {b},
+    simp only [and_true, singleton_subset_iff, mem_singleton],
+    refine ⟨hU, λ ha, (h.symm ha).elim⟩ },
+  { exact @pure_le_nhds α (nhds_adjoint a f) b },
+end
+
+lemma is_open_singleton_nhds_adjoint {α : Type*} {a b : α} (f : filter α) (hb : b ≠ a) :
+  @is_open α (nhds_adjoint a f) {b} :=
+begin
+  rw is_open_singleton_iff_nhds_eq_pure,
+  exact nhds_adjoint_nhds_of_ne a f hb
+end
+
+lemma le_nhds_adjoint_iff' {α : Type*} (a : α) (f : filter α) (t : topological_space α) :
+  t ≤ nhds_adjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, @nhds α t b = pure b :=
+begin
+  rw le_iff_nhds,
+  split,
+  { intros h,
+    split,
+    { specialize h a,
+      rwa nhds_adjoint_nhds at h },
+    { intros b hb,
+      apply le_antisymm _ (pure_le_nhds b),
+      specialize h b,
+      rwa nhds_adjoint_nhds_of_ne a f hb at h } },
+  { rintros ⟨h, h'⟩ b,
+    by_cases hb : b = a,
+    { rwa [hb, nhds_adjoint_nhds] },
+    { simp [nhds_adjoint_nhds_of_ne a f hb, h' b hb] } }
+end
+
+lemma le_nhds_adjoint_iff {α : Type*} (a : α) (f : filter α) (t : topological_space α) :
+  t ≤ nhds_adjoint a f ↔ (@nhds α t a ≤ pure a ⊔ f ∧ ∀ b, b ≠ a → t.is_open {b}) :=
+begin
+  change _ ↔ _ ∧ ∀ (b : α), b ≠ a → is_open {b},
+  rw [le_nhds_adjoint_iff', and.congr_right_iff],
+  apply λ h, forall_congr (λ b,  _),
+  rw @is_open_singleton_iff_nhds_eq_pure α t b
+end
+
 lemma nhds_infi {ι : Sort*} {t : ι → topological_space α} {a : α} :
   @nhds α (infi t) a = (⨅i, @nhds α (t i) a) := (gc_nhds a).u_infi
 

src/topology/separation.lean

@@ -282,6 +282,13 @@ class t1_space (α : Type u) [topological_space α] : Prop :=
 lemma is_closed_singleton [t1_space α] {x : α} : is_closed ({x} : set α) :=
 t1_space.t1 x
 
+lemma finite.is_closed [t1_space α] {s : set α} (hs : set.finite s) :
+  is_closed s :=
+begin
+  rw ← bUnion_of_singleton s,
+  exact is_closed_bUnion hs (λ i hi, is_closed_singleton)
+end
+
 lemma is_open_compl_singleton [t1_space α] {x : α} : is_open ({x}ᶜ : set α) :=
 is_closed_singleton.is_open_compl
 
@@ -292,6 +299,38 @@ lemma ne.nhds_within_compl_singleton [t1_space α] {x y : α} (h : x ≠ y) :
   𝓝[{y}ᶜ] x = 𝓝 x :=
 is_open_ne.nhds_within_eq h
 
+@[priority 100] -- see Note [lower instance priority]
+instance t1_space_cofinite {α : Type*} : @t1_space α (cofinite_topology α) :=
+begin
+  letI := cofinite_topology α,
+  constructor,
+  intros x,
+  rw ← is_open_compl_iff,
+  intro h,
+  simp,
+end
+
+lemma t1_space_antimono {α : Type*} : antitone (@t1_space α) :=
+begin
+  rintros t t' h ⟨ht⟩,
+  constructor,
+  intros x,
+  specialize ht x,
+  rw ← is_open_compl_iff at *,
+  exact h _ ht
+end
+
+lemma t1_space_iff_le_cofinite {α : Type*} [t : topological_space α] :
+  t1_space α ↔ t ≤ cofinite_topology α :=
+begin
+  split,
+  { introsI h U U_op,
+    rcases U.eq_empty_or_nonempty with rfl | hU,
+    { exact is_open_empty },
+    { exact (@is_closed_compl_iff α t U).mp (finite.is_closed $ U_op hU) } },
+  { exact λ h, t1_space_antimono h t1_space_cofinite }
+end
+
 lemma continuous_within_at_update_of_ne [t1_space α] [decidable_eq α] [topological_space β]
   {f : α → β} {s : set α} {x y : α} {z : β} (hne : y ≠ x) :
   continuous_within_at (function.update f x z) s y ↔ continuous_within_at f s y :=
@@ -370,13 +409,6 @@ begin
   apply is_closed_map.of_nonempty, intros s hs h2s, simp_rw [h2s.image_const, is_closed_singleton]
 end
 
-lemma finite.is_closed [t1_space α] {s : set α} (hs : set.finite s) :
-  is_closed s :=
-begin
-  rw ← bUnion_of_singleton s,
-  exact is_closed_bUnion hs (λ i hi, is_closed_singleton)
-end
-
 lemma bInter_basis_nhds [t1_space α] {ι : Sort*} {p : ι → Prop} {s : ι → set α} {x : α}
   (h : (𝓝 x).has_basis p s) : (⋂ i (h : p i), s i) = {x} :=
 begin