feat: the atTop filter is countably generated in a second-countable topology (#6864)

Author: sgouezel

Mathlib/Data/Set/Intervals/Basic.lean

@@ -1172,6 +1172,14 @@ theorem Ico_eq_Ico_iff (h : a₁ < b₁ ∨ a₂ < b₂) : Ico a₁ b₁ = Ico a
     fun ⟨h₁, h₂⟩ => by rw [h₁, h₂]⟩
 #align set.Ico_eq_Ico_iff Set.Ico_eq_Ico_iff
 
+lemma Ici_eq_singleton_iff_isTop {x : α} : (Ici x = {x}) ↔ IsTop x := by
+  refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩
+  by_contra H
+  push_neg at H
+  have : y ∈ Ici x := H.le
+  rw [h, mem_singleton_iff] at this
+  exact lt_irrefl y (this.le.trans_lt H)
+
 open Classical
 
 @[simp]

Mathlib/Order/Filter/AtTopBot.lean

@@ -132,6 +132,11 @@ theorem atTop_basis [Nonempty α] [SemilatticeSup α] : (@atTop α _).HasBasis (
   hasBasis_iInf_principal (directed_of_sup fun _ _ => Ici_subset_Ici.2)
 #align filter.at_top_basis Filter.atTop_basis
 
+theorem atTop_eq_generate_Ici [SemilatticeSup α] : atTop = generate (range (Ici (α := α))) := by
+  rcases isEmpty_or_nonempty α with hα|hα
+  · simp only [eq_iff_true_of_subsingleton]
+  · simp [(atTop_basis (α := α)).eq_generate, range]
+
 theorem atTop_basis' [SemilatticeSup α] (a : α) : (@atTop α _).HasBasis (fun x => a ≤ x) Ici :=
   ⟨fun _ =>
     (@atTop_basis α ⟨a⟩ _).mem_iff.trans
@@ -297,6 +302,18 @@ theorem OrderBot.atBot_eq (α) [PartialOrder α] [OrderBot α] : (atBot : Filter
   @OrderTop.atTop_eq αᵒᵈ _ _
 #align filter.order_bot.at_bot_eq Filter.OrderBot.atBot_eq
 
+lemma atTop_eq_pure_of_isTop [LinearOrder α] {x : α} (hx : IsTop x) :
+    (atTop : Filter α) = pure x := by
+  have : Nonempty α := ⟨x⟩
+  have : (atTop : Filter α).NeBot := atTop_basis.neBot_iff.2 (fun _ ↦ ⟨x, hx _⟩)
+  apply eq_pure_iff_singleton_mem.2
+  convert Ici_mem_atTop x using 1
+  exact (Ici_eq_singleton_iff_isTop.2 hx).symm
+
+lemma atBot_eq_pure_of_isBot [LinearOrder α] {x : α} (hx : IsBot x) :
+    (atBot : Filter α) = pure x :=
+  @atTop_eq_pure_of_isTop αᵒᵈ _ _ hx
+
 @[nontriviality]
 theorem Subsingleton.atTop_eq (α) [Subsingleton α] [Preorder α] : (atTop : Filter α) = ⊤ := by
   refine' top_unique fun s hs x => _
@@ -411,6 +428,26 @@ theorem tendsto_atBot_mono [Preorder β] {l : Filter α} {f g : α → β} (h :
   @tendsto_atTop_mono _ βᵒᵈ _ _ _ _ h
 #align filter.tendsto_at_bot_mono Filter.tendsto_atBot_mono
 
+lemma atTop_eq_generate_of_forall_exists_le [LinearOrder α] {s : Set α} (hs : ∀ x, ∃ y ∈ s, x ≤ y) :
+    (atTop : Filter α) = generate (Ici '' s) := by
+  rw [atTop_eq_generate_Ici]
+  apply le_antisymm
+  · rw [le_generate_iff]
+    rintro - ⟨y, -, rfl⟩
+    exact mem_generate_of_mem ⟨y, rfl⟩
+  · rw [le_generate_iff]
+    rintro - ⟨x, -, -, rfl⟩
+    rcases hs x with ⟨y, ys, hy⟩
+    have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
+    have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
+    exact sets_of_superset (generate (Ici '' s)) A B
+
+lemma atTop_eq_generate_of_not_bddAbove [LinearOrder α] {s : Set α} (hs : ¬ BddAbove s) :
+    (atTop : Filter α) = generate (Ici '' s) := by
+  refine' atTop_eq_generate_of_forall_exists_le fun x ↦ _
+  obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x
+  exact ⟨y, hy, hy'.le⟩
+
 end Filter
 
 namespace OrderIso

Mathlib/Order/Filter/Bases.lean

@@ -1192,6 +1192,12 @@ theorem isCountablyGenerated_top : IsCountablyGenerated (⊤ : Filter α) :=
   @principal_univ α ▸ isCountablyGenerated_principal _
 #align filter.is_countably_generated_top Filter.isCountablyGenerated_top
 
+lemma isCountablyGenerated_of_subsingleton_mem {l : Filter α} {s : Set α} (hs : s.Subsingleton)
+    (h's : s ∈ l) : IsCountablyGenerated l := by
+  rcases eq_bot_or_pure_of_subsingleton_mem hs h's with rfl|⟨x, rfl⟩
+  · exact isCountablyGenerated_bot
+  · exact isCountablyGenerated_pure x
+
 -- porting note: without explicit `Sort u` and `Type v`, Lean 4 uses `ι : Prop`
 universe u v
 

Mathlib/Order/Filter/Basic.lean

@@ -351,6 +351,9 @@ def generate (g : Set (Set α)) : Filter α where
   inter_sets := GenerateSets.inter
 #align filter.generate Filter.generate
 
+lemma mem_generate_of_mem {s : Set <| Set α} {U : Set α} (h : U ∈ s) :
+    U ∈ generate s := GenerateSets.basic h
+
 theorem le_generate_iff {s : Set (Set α)} {f : Filter α} : f ≤ generate s ↔ s ⊆ f.sets :=
   Iff.intro (fun h _ hu => h <| GenerateSets.basic <| hu) fun h _ hu =>
     hu.recOn (fun h' => h h') univ_mem (fun _ hxy hx => mem_of_superset hx hxy) fun _ _ hx hy =>
@@ -2678,6 +2681,31 @@ theorem le_pure_iff {f : Filter α} {a : α} : f ≤ pure a ↔ {a} ∈ f := by
   rw [← principal_singleton, le_principal_iff]
 #align filter.le_pure_iff Filter.le_pure_iff
 
+lemma le_pure_iff_eq_pure {l : Filter α} [hl : NeBot l] :
+    l ≤ pure x ↔ l = pure x := by
+  refine' ⟨fun h ↦ _, fun h ↦ h.le⟩
+  have hx := le_pure_iff.1 h
+  ext s
+  simp only [mem_pure]
+  refine ⟨fun h ↦ ?_, fun h ↦ mem_of_superset hx (singleton_subset_iff.2 h)⟩
+  by_contra H
+  have : s ∩ {x} ∈ l := inter_mem h hx
+  rw [inter_singleton_eq_empty.2 H, empty_mem_iff_bot] at this
+  exact NeBot.ne hl this
+
+lemma eq_pure_iff_singleton_mem {l : Filter α} [hl : NeBot l] {x : α} :
+    l = pure x ↔ {x} ∈ l := by
+  rw [← le_pure_iff_eq_pure, le_pure_iff]
+
+lemma eq_bot_or_pure_of_subsingleton_mem {l : Filter α} {s : Set α} (hs : s.Subsingleton)
+    (h's : s ∈ l) : l = ⊥ ∨ ∃ x, l = pure x := by
+  rcases l.eq_or_neBot with rfl|hl
+  · exact Or.inl rfl
+  · rcases hs.eq_empty_or_singleton with rfl|⟨x, rfl⟩
+    · rw [empty_mem_iff_bot.1 h's]
+      exact Or.inl rfl
+    · exact Or.inr ⟨x, eq_pure_iff_singleton_mem.2 h's⟩
+
 theorem mem_seq_def {f : Filter (α → β)} {g : Filter α} {s : Set β} :
     s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, (x : α → β) y ∈ s :=
   Iff.rfl

Mathlib/Topology/Order/Basic.lean

@@ -1430,6 +1430,40 @@ theorem Set.PairwiseDisjoint.countable_of_Ioo [SecondCountableTopology α] {y :
   this.of_diff countable_setOf_covby_right
 #align set.pairwise_disjoint.countable_of_Ioo Set.PairwiseDisjoint.countable_of_Ioo
 
+instance instIsCountablyGenerated_atTop [SecondCountableTopology α] :
+    IsCountablyGenerated (atTop : Filter α) := by
+  by_cases h : ∃ (x : α), IsTop x
+  · rcases h with ⟨x, hx⟩
+    rw [atTop_eq_pure_of_isTop hx]
+    exact isCountablyGenerated_pure x
+  · rcases exists_countable_basis α with ⟨b, b_count, b_ne, hb⟩
+    have : Countable b := by exact Iff.mpr countable_coe_iff b_count
+    have A : ∀ (s : b), ∃ (x : α), x ∈ (s : Set α) := by
+      intro s
+      have : (s : Set α) ≠ ∅ := by
+        intro H
+        apply b_ne
+        convert s.2
+        exact H.symm
+      exact Iff.mp nmem_singleton_empty this
+    choose a ha using A
+    have : (atTop : Filter α) = (generate (Ici '' (range a))) := by
+      apply atTop_eq_generate_of_not_bddAbove
+      intro ⟨x, hx⟩
+      simp only [IsTop, not_exists, not_forall, not_le] at h
+      rcases h x with ⟨y, hy⟩
+      obtain ⟨s, sb, -, hs⟩ : ∃ s, s ∈ b ∧ y ∈ s ∧ s ⊆ Ioi x :=
+        hb.exists_subset_of_mem_open hy isOpen_Ioi
+      have I : a ⟨s, sb⟩ ≤ x := hx (mem_range_self _)
+      have J : x < a ⟨s, sb⟩ := hs (ha ⟨s, sb⟩)
+      exact lt_irrefl _ (I.trans_lt J)
+    rw [this]
+    exact ⟨_, (countable_range _).image _, rfl⟩
+
+instance instIsCountablyGenerated_atBot [SecondCountableTopology α] :
+    IsCountablyGenerated (atBot : Filter α) :=
+  @instIsCountablyGenerated_atTop αᵒᵈ _ _ _ _
+
 section Pi
 
 /-!