refactor(order/filter/at_top): import order.filter.bases (#3523)

This way we can use facts about `filter.has_basis` in `filter.at_top`.

Also generalize `is_countably_generated_at_top_finset_nat`
to `at_top` filter on any `encodable` type.

Author: urkud

src/order/filter/at_top_bot.lean

@@ -3,7 +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, Jeremy Avigad, Yury Kudryashov, Patrick Massot
 -/
-import order.filter.basic
+import order.filter.bases
 
 /-!
 # `at_top` and `at_bot` filters on preorded sets, monoids and groups.
@@ -46,23 +46,24 @@ mem_infi_sets a $ subset.refl _
 lemma Iio_mem_at_bot [preorder α] [no_bot_order α] (x : α) : Iio x ∈ (at_bot : filter α) :=
 let ⟨z, hz⟩ := no_bot x in mem_sets_of_superset (mem_at_bot z) $ λ y h, lt_of_le_of_lt h hz
 
+lemma at_top_basis [hα : nonempty α] [semilattice_sup α] :
+  (@at_top α _).has_basis (λ _, true) Ici :=
+has_basis_infi_principal (directed_of_sup $ λ a b, Ici_subset_Ici.2) hα
+
+lemma at_top_basis' [semilattice_sup α] (a : α) :
+  (@at_top α _).has_basis (λ x, a ≤ x) Ici :=
+⟨λ t, (@at_top_basis α ⟨a⟩ _).mem_iff.trans
+  ⟨λ ⟨x, _, hx⟩, ⟨x ⊔ a, le_sup_right, λ y hy, hx (le_trans le_sup_left hy)⟩,
+    λ ⟨x, _, hx⟩, ⟨x, trivial, hx⟩⟩⟩
+
 @[instance]
 lemma at_top_ne_bot [nonempty α] [semilattice_sup α] : ne_bot (at_top : filter α) :=
-infi_ne_bot_of_directed
-  (assume a b, ⟨a ⊔ b, by simp only [ge, le_principal_iff, forall_const, set_of_subset_set_of,
-    mem_principal_sets, and_self, sup_le_iff, forall_true_iff] {contextual := tt}⟩)
-  (assume a, principal_ne_bot_iff.2 nonempty_Ici)
+at_top_basis.forall_nonempty_iff_ne_bot.1 $ λ a _, nonempty_Ici
 
 @[simp, nolint ge_or_gt]
 lemma mem_at_top_sets [nonempty α] [semilattice_sup α] {s : set α} :
   s ∈ (at_top : filter α) ↔ ∃a:α, ∀b≥a, b ∈ s :=
-let ⟨a⟩ := ‹nonempty α› in
-iff.intro
-  (assume h, infi_sets_induct h ⟨a, by simp only [forall_const, mem_univ, forall_true_iff]⟩
-    (assume a s₁ s₂ ha ⟨b, hb⟩, ⟨a ⊔ b,
-      assume c hc, ⟨ha $ le_trans le_sup_left hc, hb _ $ le_trans le_sup_right hc⟩⟩)
-    (assume s₁ s₂ h ⟨a, ha⟩, ⟨a, assume b hb, h $ ha _ hb⟩))
-  (assume ⟨a, h⟩, mem_infi_sets a $ assume x, h x)
+at_top_basis.mem_iff.trans $ exists_congr $ λ _, exists_const _
 
 @[simp, nolint ge_or_gt]
 lemma eventually_at_top [semilattice_sup α] [nonempty α] {p : α → Prop} :
@@ -71,6 +72,11 @@ mem_at_top_sets
 
 lemma eventually_ge_at_top [preorder α] (a : α) : ∀ᶠ x in at_top, a ≤ x := mem_at_top a
 
+lemma at_top_countable_basis [nonempty α] [semilattice_sup α] [encodable α] :
+  has_countable_basis (at_top : filter α) (λ _, true) Ici :=
+{ countable := countable_encodable _,
+  .. at_top_basis }
+
 lemma order_top.at_top_eq (α) [order_top α] : (at_top : filter α) = pure ⊤ :=
 le_antisymm (le_pure_iff.2 $ (eventually_ge_at_top ⊤).mono $ λ b, top_unique)
   (le_infi $ λ b, le_principal_iff.2 le_top)
@@ -109,11 +115,7 @@ frequently_at_top.mp h
 
 lemma map_at_top_eq [nonempty α] [semilattice_sup α] {f : α → β} :
   at_top.map f = (⨅a, 𝓟 $ f '' {a' | a ≤ a'}) :=
-calc map f (⨅a, 𝓟 {a' | a ≤ a'}) = (⨅a, map f $ 𝓟 {a' | a ≤ a'}) :
-    map_infi_eq (assume a b, ⟨a ⊔ b, by simp only [ge, le_principal_iff, forall_const, set_of_subset_set_of,
-      mem_principal_sets, and_self, sup_le_iff, forall_true_iff] {contextual := tt}⟩)
-      (by apply_instance)
-  ... = (⨅a, 𝓟 $ f '' {a' | a ≤ a'}) : by simp only [map_principal, eq_self_iff_true]
+(at_top_basis.map _).eq_infi
 
 lemma tendsto_at_top [preorder β] (m : α → β) (f : filter α) :
   tendsto m f at_top ↔ (∀b, ∀ᶠ a in f, b ≤ m a) :=
@@ -558,6 +560,78 @@ by rw [map_at_top_eq, map_at_top_eq];
 from (le_infi $ assume b, let ⟨v, hv⟩ := h_eq b in infi_le_of_le v $
   by simp [set.image_subset_iff]; exact hv)
 
+lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l : filter α}
+  {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s) {φ : ι → α}
+  (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l  :=
+begin
+  rw hl.to_has_basis.tendsto_right_iff,
+  intros i hi,
+  rw eventually_at_top,
+  exact ⟨i, λ j hij, hl.decreasing hi (hl.mono hij hi) hij (h j)⟩,
+end
+
+namespace is_countably_generated
+
+/-- An abstract version of continuity of sequentially continuous functions on metric spaces:
+if a filter `k` is countably generated then `tendsto f k l` iff for every sequence `u`
+converging to `k`, `f ∘ u` tends to `l`. -/
+lemma tendsto_iff_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
+  (hcb : k.is_countably_generated) :
+  tendsto f k l ↔ (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) :=
+suffices (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l,
+  from ⟨by intros; apply tendsto.comp; assumption, by assumption⟩,
+begin
+  rcases hcb.exists_antimono_seq with ⟨g, gmon, gbasis⟩,
+  have gbasis : ∀ A, A ∈ k ↔ ∃ i, g i ⊆ A,
+  { intro A,
+    subst gbasis,
+    rw mem_infi,
+    { simp only [set.mem_Union, iff_self, filter.mem_principal_sets] },
+    { exact directed_of_sup (λ i j h, principal_mono.mpr $ gmon _ _ h) },
+    { apply_instance } },
+  classical, contrapose,
+  simp only [not_forall, not_imp, not_exists, subset_def, @tendsto_def _ _ f, gbasis],
+  rintro ⟨B, hBl, hfBk⟩,
+  choose x h using hfBk,
+  use x, split,
+  { simp only [tendsto_at_top', gbasis],
+    rintros A ⟨i, hgiA⟩,
+    use i,
+    refine (λ j hj, hgiA $ gmon _ _ hj _),
+    simp only [h] },
+  { simp only [tendsto_at_top', (∘), not_forall, not_exists],
+    use [B, hBl],
+    intro i, use [i, (le_refl _)],
+    apply (h i).right },
+end
+
+lemma tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
+  (hcb : k.is_countably_generated) :
+  (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l :=
+hcb.tendsto_iff_seq_tendsto.2
+
+lemma subseq_tendsto {f : filter α} (hf : is_countably_generated f)
+  {u : ℕ → α}
+  (hx : ne_bot (f ⊓ map u at_top)) :
+  ∃ (θ : ℕ → ℕ), (strict_mono θ) ∧ (tendsto (u ∘ θ) at_top f) :=
+begin
+  rcases hf.has_antimono_basis with ⟨B, h⟩,
+  have : ∀ N, ∃ n ≥ N, u n ∈ B N,
+    from λ N, filter.inf_map_at_top_ne_bot_iff.mp hx _ (h.to_has_basis.mem_of_mem trivial) N,
+  choose φ hφ using this,
+  cases forall_and_distrib.mp hφ with φ_ge φ_in,
+  have lim_uφ : tendsto (u ∘ φ) at_top f,
+    from h.tendsto φ_in,
+  have lim_φ : tendsto φ at_top at_top,
+    from (tendsto_at_top_mono φ_ge tendsto_id),
+  obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, strict_mono ψ ∧ strict_mono (φ ∘ ψ),
+    from strict_mono_subseq_of_tendsto_at_top lim_φ,
+  exact ⟨φ ∘ ψ, hψφ, lim_uφ.comp $ strict_mono_tendsto_at_top hψ⟩,
+end
+
+end is_countably_generated
+
+
 end filter
 
 open filter finset

src/order/filter/bases.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Yury Kudryashov, Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
-import order.filter.at_top_bot
+import order.filter.basic
 import data.set.countable
 
 /-!
@@ -266,16 +266,6 @@ begin
     tauto }
 end
 
-lemma at_top_basis [nonempty α] [semilattice_sup α] :
-  (@at_top α _).has_basis (λ _, true) Ici :=
-⟨λ t, by simpa only [exists_prop, true_and] using @mem_at_top_sets α _ _ t⟩
-
-lemma at_top_basis' [semilattice_sup α] (a : α) :
-  (@at_top α _).has_basis (λ x, a ≤ x) Ici :=
-⟨λ t, (@at_top_basis α ⟨a⟩ _).mem_iff.trans
-  ⟨λ ⟨x, _, hx⟩, ⟨x ⊔ a, le_sup_right, λ y hy, hx (le_trans le_sup_left hy)⟩,
-    λ ⟨x, _, hx⟩, ⟨x, trivial, hx⟩⟩⟩
-
 theorem has_basis.ge_iff (hl' : l'.has_basis p' s')  : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l :=
 ⟨λ h i' hi', h $ hl'.mem_of_mem hi',
   λ h s hs, let ⟨i', hi', hs⟩ := hl'.mem_iff.1 hs in mem_sets_of_superset (h _ hi') hs⟩
@@ -465,16 +455,6 @@ lemma has_basis.prod' {la : filter α} {lb : filter β} {ι : Type*} {p : ι →
     exact ⟨sa i, hla.mem_of_mem hi, sb i, hlb.mem_of_mem hi, h⟩ },
 end⟩
 
-lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l : filter α}
-  {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s) {φ : ι → α}
-  (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l  :=
-begin
-  rw hl.to_has_basis.tendsto_right_iff,
-  intros i hi,
-  rw eventually_at_top,
-  exact ⟨i, λ j hij, hl.decreasing hi (hl.mono hij hi) hij (h j)⟩,
-end
-
 end two_types
 
 /-- `is_countably_generated f` means `f = generate s` for some countable `s`. -/
@@ -612,6 +592,11 @@ end
 
 end is_countably_generated
 
+lemma has_countable_basis.is_countably_generated {f : filter α} {p : ι → Prop} {s : ι → set α}
+  (h : f.has_countable_basis p s) :
+  f.is_countably_generated :=
+⟨{t | ∃ i, p i ∧ s i = t}, h.countable.image s, h.to_has_basis.eq_generate⟩
+
 lemma is_countably_generated_seq (x : ℕ → set α) : is_countably_generated (⨅ i, 𝓟 $ x i) :=
 begin
   rcases antimono_seq_of_seq x with ⟨y, am, h⟩,
@@ -660,78 +645,6 @@ begin
           ... = (⨅ i, comap f $ 𝓟 $ x i) : comap_infi
           ... = (⨅ i, 𝓟 $ f ⁻¹' x i)     : by simp_rw comap_principal,
 end
-
-/-- An abstract version of continuity of sequentially continuous functions on metric spaces:
-if a filter `k` is countably generated then `tendsto f k l` iff for every sequence `u`
-converging to `k`, `f ∘ u` tends to `l`. -/
-lemma tendsto_iff_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
-  (hcb : k.is_countably_generated) :
-  tendsto f k l ↔ (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) :=
-suffices (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l,
-  from ⟨by intros; apply tendsto.comp; assumption, by assumption⟩,
-begin
-  rcases hcb.exists_antimono_seq with ⟨g, gmon, gbasis⟩,
-  have gbasis : ∀ A, A ∈ k ↔ ∃ i, g i ⊆ A,
-  { intro A,
-    subst gbasis,
-    rw mem_infi,
-    { simp only [set.mem_Union, iff_self, filter.mem_principal_sets] },
-    { exact directed_of_sup (λ i j h, principal_mono.mpr $ gmon _ _ h) },
-    { apply_instance } },
-  classical, contrapose,
-  simp only [not_forall, not_imp, not_exists, subset_def, @tendsto_def _ _ f, gbasis],
-  rintro ⟨B, hBl, hfBk⟩,
-  choose x h using hfBk,
-  use x, split,
-  { simp only [tendsto_at_top', gbasis],
-    rintros A ⟨i, hgiA⟩,
-    use i,
-    refine (λ j hj, hgiA $ gmon _ _ hj _),
-    simp only [h] },
-  { simp only [tendsto_at_top', (∘), not_forall, not_exists],
-    use [B, hBl],
-    intro i, use [i, (le_refl _)],
-    apply (h i).right },
-end
-
-lemma tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
-  (hcb : k.is_countably_generated) :
-  (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l :=
-hcb.tendsto_iff_seq_tendsto.2
-
-lemma subseq_tendsto {f : filter α} (hf : is_countably_generated f)
-  {u : ℕ → α}
-  (hx : ne_bot (f ⊓ map u at_top)) :
-  ∃ (θ : ℕ → ℕ), (strict_mono θ) ∧ (tendsto (u ∘ θ) at_top f) :=
-begin
-  rcases hf.has_antimono_basis with ⟨B, h⟩,
-  have : ∀ N, ∃ n ≥ N, u n ∈ B N,
-    from λ N, filter.inf_map_at_top_ne_bot_iff.mp hx _ (h.to_has_basis.mem_of_mem trivial) N,
-  choose φ hφ using this,
-  cases forall_and_distrib.mp hφ with φ_ge φ_in,
-  have lim_uφ : tendsto (u ∘ φ) at_top f,
-    from h.tendsto φ_in,
-  have lim_φ : tendsto φ at_top at_top,
-    from (tendsto_at_top_mono φ_ge tendsto_id),
-  obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, strict_mono ψ ∧ strict_mono (φ ∘ ψ),
-    from strict_mono_subseq_of_tendsto_at_top lim_φ,
-  exact ⟨φ ∘ ψ, hψφ, lim_uφ.comp $ strict_mono_tendsto_at_top hψ⟩,
-end
-
 end is_countably_generated
 
--- TODO : prove this for a encodable type
-lemma is_countably_generated_at_top_finset_nat : (at_top : filter $ finset ℕ).is_countably_generated :=
-begin
-  apply is_countably_generated_of_seq,
-  use λ N, Ici (finset.range N),
-  apply eq_infi_of_mem_sets_iff_exists_mem,
-  assume s,
-  rw mem_at_top_sets,
-  refine ⟨_, λ ⟨N, hN⟩, ⟨finset.range N, hN⟩⟩,
-  rintros ⟨t, ht⟩,
-  rcases mem_at_top_sets.1 (tendsto_finset_range (mem_at_top t)) with ⟨N, hN⟩,
-  simp only [preimage, mem_set_of_eq] at hN,
-  exact ⟨N, mem_principal_sets.2 $ λ t' ht', ht t' $ le_trans (hN _ $ le_refl N) ht'⟩
-end
 end filter